{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}
module Data.Comp.Sum
(
(:<:),
(:=:),
(:+:),
caseF,
proj,
project,
deepProject,
project_,
deepProject_,
inj,
inject,
deepInject,
inject_,
deepInject_,
split,
injectConst,
projectConst,
injectCxt,
liftCxt,
substHoles,
substHoles'
) where
import Data.Comp.Algebra
import Data.Comp.Ops
import Data.Comp.Term
import Control.Monad hiding (mapM, sequence)
import Prelude hiding (mapM, sequence)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe
project :: (g :<: f) => Cxt h f a -> Maybe (g (Cxt h f a))
project :: forall (g :: * -> *) (f :: * -> *) h a.
(g :<: f) =>
Cxt h f a -> Maybe (g (Cxt h f a))
project = forall (f :: * -> *) (g :: * -> *) h a.
SigFunM Maybe f g -> Cxt h f a -> Maybe (g (Cxt h f a))
project_ forall (f :: * -> *) (g :: * -> *) a.
(f :<: g) =>
g a -> Maybe (f a)
proj
project_ :: SigFunM Maybe f g -> Cxt h f a -> Maybe (g (Cxt h f a))
project_ :: forall (f :: * -> *) (g :: * -> *) h a.
SigFunM Maybe f g -> Cxt h f a -> Maybe (g (Cxt h f a))
project_ SigFunM Maybe f g
_ (Hole a
_) = forall a. Maybe a
Nothing
project_ SigFunM Maybe f g
f (Term f (Cxt h f a)
t) = SigFunM Maybe f g
f f (Cxt h f a)
t
deepProject :: (Traversable g, g :<: f) => CxtFunM Maybe f g
{-# INLINE deepProject #-}
deepProject :: forall (g :: * -> *) (f :: * -> *).
(Traversable g, g :<: f) =>
CxtFunM Maybe f g
deepProject = forall (g :: * -> *) (m :: * -> *) (f :: * -> *).
(Traversable g, Monad m) =>
SigFunM m f g -> CxtFunM m f g
appSigFunM' forall (f :: * -> *) (g :: * -> *) a.
(f :<: g) =>
g a -> Maybe (f a)
proj
deepProject_ :: (Traversable g) => (SigFunM Maybe f g) -> CxtFunM Maybe f g
{-# INLINE deepProject_ #-}
deepProject_ :: forall (g :: * -> *) (f :: * -> *).
Traversable g =>
SigFunM Maybe f g -> CxtFunM Maybe f g
deepProject_ = forall (g :: * -> *) (m :: * -> *) (f :: * -> *).
(Traversable g, Monad m) =>
SigFunM m f g -> CxtFunM m f g
appSigFunM'
inject :: (g :<: f) => g (Cxt h f a) -> Cxt h f a
inject :: forall (g :: * -> *) (f :: * -> *) h a.
(g :<: f) =>
g (Cxt h f a) -> Cxt h f a
inject = forall (g :: * -> *) (f :: * -> *) h a.
SigFun g f -> g (Cxt h f a) -> Cxt h f a
inject_ forall (f :: * -> *) (g :: * -> *) a. (f :<: g) => f a -> g a
inj
inject_ :: SigFun g f -> g (Cxt h f a) -> Cxt h f a
inject_ :: forall (g :: * -> *) (f :: * -> *) h a.
SigFun g f -> g (Cxt h f a) -> Cxt h f a
inject_ SigFun g f
f = forall (b :: * -> *) a c. b (Cxt a b c) -> Cxt a b c
Term forall b c a. (b -> c) -> (a -> b) -> a -> c
. SigFun g f
f
deepInject :: (Functor g, g :<: f) => CxtFun g f
{-# INLINE deepInject #-}
deepInject :: forall (g :: * -> *) (f :: * -> *).
(Functor g, g :<: f) =>
CxtFun g f
deepInject = forall (g :: * -> *) (f :: * -> *).
Functor g =>
SigFun g f -> CxtFun g f
deepInject_ forall (f :: * -> *) (g :: * -> *) a. (f :<: g) => f a -> g a
inj
deepInject_ :: (Functor g) => SigFun g f -> CxtFun g f
{-# INLINE deepInject_ #-}
deepInject_ :: forall (g :: * -> *) (f :: * -> *).
Functor g =>
SigFun g f -> CxtFun g f
deepInject_ = forall (g :: * -> *) (f :: * -> *).
Functor g =>
SigFun g f -> CxtFun g f
appSigFun
split :: (f :=: f1 :+: f2) => (f1 (Term f) -> a) -> (f2 (Term f) -> a) -> Term f -> a
split :: forall (f :: * -> *) (f1 :: * -> *) (f2 :: * -> *) a.
(f :=: (f1 :+: f2)) =>
(f1 (Term f) -> a) -> (f2 (Term f) -> a) -> Term f -> a
split f1 (Term f) -> a
f1 f2 (Term f) -> a
f2 (Term f (Term f)
t) = forall (f :: * -> *) (f1 :: * -> *) (f2 :: * -> *) a b.
(f :=: (f1 :+: f2)) =>
(f1 a -> b) -> (f2 a -> b) -> f a -> b
spl f1 (Term f) -> a
f1 f2 (Term f) -> a
f2 f (Term f)
t
injectConst :: (Functor g, g :<: f) => Const g -> Cxt h f a
injectConst :: forall (g :: * -> *) (f :: * -> *) h a.
(Functor g, g :<: f) =>
Const g -> Cxt h f a
injectConst = forall (g :: * -> *) (f :: * -> *) h a.
(g :<: f) =>
g (Cxt h f a) -> Cxt h f a
inject forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. a -> b -> a
const forall a. HasCallStack => a
undefined)
projectConst :: (Functor g, g :<: f) => Cxt h f a -> Maybe (Const g)
projectConst :: forall (g :: * -> *) (f :: * -> *) h a.
(Functor g, g :<: f) =>
Cxt h f a -> Maybe (Const g)
projectConst = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. a -> b -> a
const ())) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (g :: * -> *) (f :: * -> *) h a.
(g :<: f) =>
Cxt h f a -> Maybe (g (Cxt h f a))
project
injectCxt :: (Functor g, g :<: f) => Cxt h' g (Cxt h f a) -> Cxt h f a
injectCxt :: forall (g :: * -> *) (f :: * -> *) h' h a.
(Functor g, g :<: f) =>
Cxt h' g (Cxt h f a) -> Cxt h f a
injectCxt = forall (f :: * -> *) a h. Functor f => Alg f a -> Cxt h f a -> a
cata' forall (g :: * -> *) (f :: * -> *) h a.
(g :<: f) =>
g (Cxt h f a) -> Cxt h f a
inject
liftCxt :: (Functor f, g :<: f) => g a -> Context f a
liftCxt :: forall (f :: * -> *) (g :: * -> *) a.
(Functor f, g :<: f) =>
g a -> Context f a
liftCxt g a
g = forall (f :: * -> *) a. Functor f => f a -> Context f a
simpCxt forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) (g :: * -> *) a. (f :<: g) => f a -> g a
inj g a
g
substHoles :: (Functor f, Functor g, f :<: g) => Cxt h' f v -> (v -> Cxt h g a) -> Cxt h g a
substHoles :: forall (f :: * -> *) (g :: * -> *) h' v h a.
(Functor f, Functor g, f :<: g) =>
Cxt h' f v -> (v -> Cxt h g a) -> Cxt h g a
substHoles Cxt h' f v
c v -> Cxt h g a
f = forall (g :: * -> *) (f :: * -> *) h' h a.
(Functor g, g :<: f) =>
Cxt h' g (Cxt h f a) -> Cxt h f a
injectCxt forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap v -> Cxt h g a
f Cxt h' f v
c
substHoles' :: (Functor f, Functor g, f :<: g, Ord v) => Cxt h' f v -> Map v (Cxt h g a) -> Cxt h g a
substHoles' :: forall (f :: * -> *) (g :: * -> *) v h' h a.
(Functor f, Functor g, f :<: g, Ord v) =>
Cxt h' f v -> Map v (Cxt h g a) -> Cxt h g a
substHoles' Cxt h' f v
c Map v (Cxt h g a)
m = forall (f :: * -> *) (g :: * -> *) h' v h a.
(Functor f, Functor g, f :<: g) =>
Cxt h' f v -> (v -> Cxt h g a) -> Cxt h g a
substHoles Cxt h' f v
c (forall a. HasCallStack => Maybe a -> a
fromJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall k a. Ord k => k -> Map k a -> Maybe a
`Map.lookup` Map v (Cxt h g a)
m))
instance (Show (f a), Show (g a)) => Show ((f :+: g) a) where
show :: (:+:) f g a -> String
show (Inl f a
v) = forall a. Show a => a -> String
show f a
v
show (Inr g a
v) = forall a. Show a => a -> String
show g a
v
instance (Ord (f a), Ord (g a)) => Ord ((f :+: g) a) where
compare :: (:+:) f g a -> (:+:) f g a -> Ordering
compare (Inl f a
_) (Inr g a
_) = Ordering
LT
compare (Inr g a
_) (Inl f a
_) = Ordering
GT
compare (Inl f a
x) (Inl f a
y) = forall a. Ord a => a -> a -> Ordering
compare f a
x f a
y
compare (Inr g a
x) (Inr g a
y) = forall a. Ord a => a -> a -> Ordering
compare g a
x g a
y
instance (Eq (f a), Eq (g a)) => Eq ((f :+: g) a) where
(Inl f a
x) == :: (:+:) f g a -> (:+:) f g a -> Bool
== (Inl f a
y) = f a
x forall a. Eq a => a -> a -> Bool
== f a
y
(Inr g a
x) == (Inr g a
y) = g a
x forall a. Eq a => a -> a -> Bool
== g a
y
(:+:) f g a
_ == (:+:) f g a
_ = Bool
False