{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Comp.Multi.Strategy.Classification
(
DynCase(..)
, KDynCase(..)
, dynProj
, fromDynProj
, caseE
, caseDyn
, subterms
, isSort
, kIsSort
) where
import Data.Type.Equality ( (:~:)(..), gcastWith )
import Data.Maybe ( fromJust )
import Data.Proxy
import GHC.Exts ( Constraint )
import Data.Comp.Multi ( HFix, Sum, E, K, runE, caseH, (:&:), remA, Cxt(..), subs, NotSum, All, caseCxt )
import Data.Comp.Multi.HFoldable ( HFoldable )
class EmptyConstraint (e :: * -> *) l
instance EmptyConstraint e l
class DynCase f a where
dyncase :: f b -> Maybe (b :~: a)
class KDynCase (f :: (* -> *) -> * -> *) a where
kdyncase :: f e b -> Maybe (b :~: a)
instance {-# OVERLAPPABLE #-} (NotSum f) => KDynCase f a where
kdyncase :: f e b -> Maybe (b :~: a)
kdyncase = Maybe (b :~: a) -> f e b -> Maybe (b :~: a)
forall a b. a -> b -> a
const Maybe (b :~: a)
forall a. Maybe a
Nothing
class (KDynCase f l ) => KDynCaseFlip l f
instance (KDynCase f l) => KDynCaseFlip l f
instance {-# OVERLAPPING #-} (All (KDynCaseFlip l) fs) => KDynCase (Sum fs) l where
kdyncase :: Sum fs e b -> Maybe (b :~: l)
kdyncase = Proxy (KDynCaseFlip l)
-> (forall (f :: (* -> *) -> * -> *).
KDynCaseFlip l f =>
f e b -> Maybe (b :~: l))
-> Sum fs e b
-> Maybe (b :~: l)
forall (cxt :: ((* -> *) -> * -> *) -> Constraint)
(fs :: [(* -> *) -> * -> *]) (a :: * -> *) e b.
All cxt fs =>
Proxy cxt
-> (forall (f :: (* -> *) -> * -> *). cxt f => f a e -> b)
-> Sum fs a e
-> b
caseCxt (Proxy (KDynCaseFlip l)
forall k (t :: k). Proxy t
Proxy :: Proxy (KDynCaseFlip l)) forall (f :: (* -> *) -> * -> *).
KDynCaseFlip l f =>
f e b -> Maybe (b :~: l)
forall (f :: (* -> *) -> * -> *) a (e :: * -> *) b.
KDynCase f a =>
f e b -> Maybe (b :~: a)
kdyncase
instance {-# OVERLAPPING #-} (KDynCase f l) => KDynCase (f :&: a) l where
kdyncase :: (:&:) f a e b -> Maybe (b :~: l)
kdyncase = f e b -> Maybe (b :~: l)
forall (f :: (* -> *) -> * -> *) a (e :: * -> *) b.
KDynCase f a =>
f e b -> Maybe (b :~: a)
kdyncase (f e b -> Maybe (b :~: l))
-> ((:&:) f a e b -> f e b) -> (:&:) f a e b -> Maybe (b :~: l)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:&:) f a e b -> f e b
forall (s :: (* -> *) -> * -> *) (s' :: (* -> *) -> * -> *)
(a :: * -> *).
RemA s s' =>
s a :-> s' a
remA
instance DynCase (K a) b where
dyncase :: K a b -> Maybe (b :~: b)
dyncase _ = Maybe (b :~: b)
forall a. Maybe a
Nothing
instance (KDynCase f l, DynCase a l) => DynCase (Cxt h f a) l where
dyncase :: Cxt h f a b -> Maybe (b :~: l)
dyncase (Term x :: f (Cxt h f a) b
x) = f (Cxt h f a) b -> Maybe (b :~: l)
forall (f :: (* -> *) -> * -> *) a (e :: * -> *) b.
KDynCase f a =>
f e b -> Maybe (b :~: a)
kdyncase f (Cxt h f a) b
x
dyncase (Hole x :: a b
x) = a b -> Maybe (b :~: l)
forall (f :: * -> *) a b. DynCase f a => f b -> Maybe (b :~: a)
dyncase a b
x
dynProj :: forall f l l'. (DynCase f l) => f l' -> Maybe (f l)
dynProj :: f l' -> Maybe (f l)
dynProj x :: f l'
x = case (f l' -> Maybe (l' :~: l)
forall (f :: * -> *) a b. DynCase f a => f b -> Maybe (b :~: a)
dyncase f l'
x :: Maybe (l' :~: l)) of
Just p :: l' :~: l
p -> f l -> Maybe (f l)
forall a. a -> Maybe a
Just ((l' :~: l) -> ((l' ~ l) => f l) -> f l
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith l' :~: l
p f l'
(l' ~ l) => f l
x)
Nothing -> Maybe (f l)
forall a. Maybe a
Nothing
fromDynProj :: (DynCase f l) => f l' -> f l
fromDynProj :: f l' -> f l
fromDynProj x :: f l'
x = Maybe (f l) -> f l
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (f l) -> f l) -> Maybe (f l) -> f l
forall a b. (a -> b) -> a -> b
$ f l' -> Maybe (f l)
forall (f :: * -> *) l l'. DynCase f l => f l' -> Maybe (f l)
dynProj f l'
x
caseE :: (DynCase f l) => E f -> Maybe (f l)
caseE :: E f -> Maybe (f l)
caseE = (f :=> Maybe (f l)) -> E f -> Maybe (f l)
forall (f :: * -> *) b. (f :=> b) -> E f -> b
runE f :=> Maybe (f l)
forall (f :: * -> *) l l'. DynCase f l => f l' -> Maybe (f l)
dynProj
caseDyn :: (DynCase f l)
=> (f l -> r)
-> f i
-> r
-> r
caseDyn :: (f l -> r) -> f i -> r -> r
caseDyn f :: f l -> r
f t :: f i
t r :: r
r = r -> (f l -> r) -> Maybe (f l) -> r
forall b a. b -> (a -> b) -> Maybe a -> b
maybe r
r f l -> r
f (f i -> Maybe (f l)
forall (f :: * -> *) l l'. DynCase f l => f l' -> Maybe (f l)
dynProj f i
t)
subterms :: (DynCase (HFix f) l, HFoldable f) => HFix f l' -> [HFix f l]
subterms :: HFix f l' -> [HFix f l]
subterms x :: HFix f l'
x = [ HFix f l
y | Just y :: HFix f l
y <- (E (HFix f) -> Maybe (HFix f l))
-> [E (HFix f)] -> [Maybe (HFix f l)]
forall a b. (a -> b) -> [a] -> [b]
map E (HFix f) -> Maybe (HFix f l)
forall (f :: * -> *) l. DynCase f l => E f -> Maybe (f l)
caseE ([E (HFix f)] -> [Maybe (HFix f l)])
-> [E (HFix f)] -> [Maybe (HFix f l)]
forall a b. (a -> b) -> a -> b
$ HFix f l' -> [E (HFix f)]
forall (f :: (* -> *) -> * -> *).
HFoldable f =>
HFix f :=> [E (HFix f)]
subs HFix f l'
x]
isSort :: forall e l. (DynCase e l) => Proxy l -> forall i. e i -> Bool
isSort :: Proxy l -> forall i. e i -> Bool
isSort _ x :: e i
x = case (e i -> Maybe (i :~: l)
forall (f :: * -> *) a b. DynCase f a => f b -> Maybe (b :~: a)
dyncase e i
x :: Maybe (_ :~: l)) of
Just _ -> Bool
True
Nothing -> Bool
False
kIsSort :: forall f l. (KDynCase f l) => Proxy l -> forall i e. f e i -> Bool
kIsSort :: Proxy l -> forall i (e :: * -> *). f e i -> Bool
kIsSort _ x :: f e i
x = case (f e i -> Maybe (i :~: l)
forall (f :: (* -> *) -> * -> *) a (e :: * -> *) b.
KDynCase f a =>
f e b -> Maybe (b :~: a)
kdyncase f e i
x :: Maybe (_ :~: l)) of
Just _ -> Bool
True
Nothing -> Bool
False