module Control.Get where
import Data.Singletons.Prelude.Bool
import Data.Proxy
import Data.Constraint (Dict(..), withDict)
data And x y = And x y
data Or x y = OrLeft x | OrRight y
data Bottom
fromBot :: Bottom -> a
fromBot bot = case bot of
data Top = Top
fromVal :: a -> Proxy a
fromVal _ = Proxy
class TryGet as from self ok | as from self -> ok where
tryGetSing :: Proxy self -> Proxy from -> Proxy as -> Sing ok
tryGetVal :: self -> from -> Proxy as -> If ok as ()
tryGet :: self -> from -> Proxy as -> (If ok as (), Sing ok)
tryGet self from p = (tryGetVal self from p, tryGetSing (fromVal self) (fromVal from) p)
class TryGet as from from True => Get as from where
get :: from -> as
get f = res where
res = tryGetVal f f (fromVal res)
instance TryGet as from from True => Get as from
instance TryGet Top from self True where
tryGetVal _ _ _ = Top
tryGetSing _ _ _ = STrue
instance ok ~ False => TryGet as Top self ok where
tryGetVal _ _ _ = ()
tryGetSing _ _ _ = SFalse
instance TryGet as Bottom self True where
tryGetVal _ bot _ = fromBot bot
tryGetSing _ _ _ = STrue
andLeftP :: Proxy (And l r) -> Proxy l
andLeftP _ = Proxy
andRightP :: Proxy (And l r) -> Proxy r
andRightP _ = Proxy
class TryGetAndL a b from self (aOK :: Bool) (andOK :: Bool) | b from self aOK -> andOK where
tryGetAndLVal :: self -> from -> (If aOK a (), Sing aOK) -> Proxy (And a b) -> If andOK (And a b) ()
tryGetAndLSing :: Proxy self -> Proxy from -> Sing aOK -> Proxy (And a b) -> Sing andOK
instance TryGetAndL a b from self False False where
tryGetAndLVal _ _ _ _ = ()
tryGetAndLSing _ _ _ _ = SFalse
instance TryGet b from self andOK => TryGetAndL a b from self True andOK where
tryGetAndLVal self from (a, _) p = let (b, s) = tryGet self from (andRightP p) in
case s of
STrue -> And a b
SFalse -> ()
tryGetAndLSing self from _ p = tryGetSing self from (andRightP p)
instance (TryGet a from self aOK, TryGetAndL a b from self aOK andOK) => TryGet (And a b) from self andOK where
tryGetVal self from p = tryGetAndLVal self from (tryGet self from (andLeftP p)) p
tryGetSing self from p = tryGetAndLSing self from (tryGetSing self from (andLeftP p)) p
class TryGetAndR as b self (aOK :: Bool) (andOK :: Bool) | as b self aOK -> andOK where
tryGetAndRVal :: self -> (If aOK as (), Sing aOK) -> b -> Proxy as -> If andOK as ()
tryGetAndRSing :: Proxy self -> Sing aOK -> Proxy b -> Proxy as -> Sing andOK
instance TryGetAndR as b self True True where
tryGetAndRVal _ (a, _) _ _ = a
tryGetAndRSing _ _ _ _ = STrue
instance TryGet as b self andOK => TryGetAndR as b self False andOK where
tryGetAndRVal self _ b p = tryGetVal self b p
tryGetAndRSing self _ from p = tryGetSing self from p
instance (TryGet as a self aOK, TryGetAndR as b self aOK andOK) => TryGet as (And a b) self andOK where
tryGetVal self (And a b) p = tryGetAndRVal self (tryGet self a p) b p
tryGetSing self from p = tryGetAndRSing self (tryGetSing self (andLeftP from) p) (andRightP from) p
orLeftP :: Proxy (Or l r) -> Proxy l
orLeftP _ = Proxy
orRightP :: Proxy (Or l r) -> Proxy r
orRightP _ = Proxy
class TryGetOrL a b from self (aOK :: Bool) (orOK :: Bool) | b from self aOK -> orOK where
tryGetOrLVal :: self -> from -> (If aOK a (), Sing aOK) -> Proxy (Or a b) -> If orOK (Or a b) ()
tryGetOrLSing :: Proxy self -> Proxy from -> Sing aOK -> Proxy (Or a b) -> Sing orOK
instance TryGetOrL a b from self True True where
tryGetOrLVal _ _ (a, _) _ = OrLeft a
tryGetOrLSing _ _ _ _ = STrue
instance TryGet b from self orOK => TryGetOrL a b from self False orOK where
tryGetOrLVal self from _ p = let (b, s) = tryGet self from (orRightP p) in
case s of
STrue -> OrRight b
SFalse -> ()
tryGetOrLSing self from _ p = tryGetSing self from (orRightP p)
instance (TryGet a from self aOK, TryGetOrL a b from self aOK orOK) => TryGet (Or a b) from self orOK where
tryGetVal self from p = tryGetOrLVal self from (tryGet self from (orLeftP p)) p
tryGetSing self from p = tryGetOrLSing self from (tryGetSing self from (orLeftP p)) p
class TryGetOrR as b self (aOK :: Bool) orOK | as b self aOK -> orOK where
tryGetOrRVal :: self -> b -> Sing aOK -> Proxy as -> If orOK as ()
tryGetOrRSing :: Proxy self -> Proxy b -> Sing aOK -> Proxy as -> Sing orOK
tryGetOrRUnify :: Proxy self -> Proxy b -> Sing aOK -> Proxy as -> Dict (orOK ~ True) -> Dict (aOK ~ True)
instance TryGetOrR as b self False False where
tryGetOrRVal _ _ _ _ = ()
tryGetOrRSing _ _ _ _ = SFalse
tryGetOrRUnify _ _ _ _ x = x
instance TryGet as b self orOK => TryGetOrR as b self True orOK where
tryGetOrRVal self b _ p = tryGetVal self b p
tryGetOrRSing self b _ p = tryGetSing self b p
tryGetOrRUnify _ _ _ _ _ = Dict
instance (TryGet as a self aOK, TryGetOrR as b self aOK orOK) => TryGet as (Or a b) self orOK where
tryGetVal self o@(OrLeft a) p =
let
oP = fromVal o
orP = orRightP oP
selfP = fromVal self
singL = tryGetSing selfP (fromVal a) p
in
case tryGetOrRSing (fromVal self) orP singL p of
STrue -> tryGetOrRUnify selfP orP singL p Dict `withDict` tryGetVal self a p
SFalse -> ()
tryGetVal self o@(OrRight b) p = tryGetOrRVal self b (tryGetSing (fromVal self) (orLeftP $ fromVal o) p) p
tryGetSing self from p = tryGetOrRSing self (orRightP from) (tryGetSing self (orLeftP from) p) p
instance ok ~ True => TryGet a a self ok where
tryGetVal _ a _ = a
tryGetSing _ _ _ = STrue
newtype Protected x = Protected { runProtected :: x }
unProtectedP :: Proxy (Protected x) -> Proxy x
unProtectedP _ = Proxy
instance TryGet as from from ok => TryGet as (Protected from) self ok where
tryGetVal self (Protected from) p = tryGetVal from from p
tryGetSing _ pFrom p = let from = unProtectedP pFrom in tryGetSing from from p