module Annotations.MultiRec.Any
( Any(..), mkAny, matchAny
, AnyF(..), mkAnyF, matchAnyF, unwrapAnyF, ($?)
) where
import Annotations.MultiRec.ShowFam
import Generics.MultiRec
data Any s where
Any :: s ix -> ix -> Any s
instance ShowFam s => Show (Any s) where
show = showAny
showAny :: ShowFam s => Any s -> String
showAny (Any w x) = showFam w x
mkAny :: El s ix => ix -> Any s
mkAny = Any proof
matchAny :: forall s a. EqS s => s a -> Any s -> Maybe a
matchAny p (Any w x) = match' w x p where
match' :: forall b. s b -> b -> s a -> Maybe a
match' w x w' = case eqS w w' of
Nothing -> Nothing
Just Refl -> Just x
data AnyF s f where
AnyF :: s ix -> f ix -> AnyF s f
mkAnyF :: El s ix => r ix -> AnyF s r
mkAnyF = AnyF proof
matchAnyF :: forall s f a. EqS s => s a -> AnyF s f -> Maybe (f a)
matchAnyF p (AnyF w x) = match' w x p where
match' :: forall b. s b -> f b -> s a -> Maybe (f a)
match' w x w' = case eqS w w' of
Nothing -> Nothing
Just Refl -> Just x
($?) :: (forall b. s b -> f b -> a) -> AnyF s f -> a
f $? (AnyF p x) = f p x
unwrapAnyF :: (forall ix. f ix -> ix) -> AnyF s f -> Any s
unwrapAnyF g (AnyF ix rix) = Any ix (g rix)