{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE UnicodeSyntax #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ViewPatterns #-}
module Control.Category.Constrained.Reified.PolyPattern (
#if __GLASGOW_HASKELL__ > 708
pattern Specific, pattern Id, pattern (:<<<), pattern (:>>>)
, pattern Swap
, pattern AttachUnit, pattern DetachUnit
, pattern Regroup, pattern Regroup'
, pattern (:***)
, pattern (:&&&), pattern Fst, pattern Snd, pattern Terminal
, pattern Const,
#endif
CRCategory(..), CRCartesian(..), CRMorphism(..), CRPreArrow(..), CRWellPointed(..)
) where
import Prelude ()
import GHC.Exts (Constraint)
import Control.Category.Constrained.Prelude
import Control.Arrow.Constrained
import Control.Category.Constrained.Reified
import Data.Tagged
#if __GLASGOW_HASKELL__ > 708
infixr 1 :<<<, :>>>
#endif
data IdPattern k α β where
IsId :: Object k α => IdPattern k α α
NotId :: IdPattern k α β
data CompoPattern k α β where
IsCompo :: Object k β
=> k α β -> k β γ -> CompoPattern k α γ
NotCompo :: CompoPattern k α β
class Category k => CRCategory k where
type SpecificCat k :: * -> * -> *
fromSpecific :: SpecificCat k α β -> k α β
match_concrete :: k α β -> Maybe (SpecificCat k α β)
match_id :: k α β -> IdPattern k α β
match_compose :: k α β -> CompoPattern k α β
instance Category k => CRCategory (ReCategory k) where
type SpecificCat (ReCategory k) = k
fromSpecific :: SpecificCat (ReCategory k) α β -> ReCategory k α β
fromSpecific = SpecificCat (ReCategory k) α β -> ReCategory k α β
forall (k :: * -> * -> *) α β. k α β -> ReCategory k α β
ReCategory
match_concrete :: ReCategory k α β -> Maybe (SpecificCat (ReCategory k) α β)
match_concrete (ReCategory k α β
f) = k α β -> Maybe (k α β)
forall a. a -> Maybe a
Just k α β
f
match_concrete ReCategory k α β
_ = Maybe (SpecificCat (ReCategory k) α β)
forall a. Maybe a
Nothing
match_id :: ReCategory k α β -> IdPattern (ReCategory k) α β
match_id ReCategory k α β
CategoryId = IdPattern (ReCategory k) α β
forall (k :: * -> * -> *) α. Object k α => IdPattern k α α
IsId
match_id ReCategory k α β
_ = IdPattern (ReCategory k) α β
forall (k :: * -> * -> *) α β. IdPattern k α β
NotId
match_compose :: ReCategory k α β -> CompoPattern (ReCategory k) α β
match_compose (CategoryCompo ReCategory k α β
f ReCategory k β β
g) = ReCategory k α β
-> ReCategory k β β -> CompoPattern (ReCategory k) α β
forall (k :: * -> * -> *) β α γ.
Object k β =>
k α β -> k β γ -> CompoPattern k α γ
IsCompo ReCategory k α β
f ReCategory k β β
g
match_compose ReCategory k α β
_ = CompoPattern (ReCategory k) α β
forall (k :: * -> * -> *) α β. CompoPattern k α β
NotCompo
#if __GLASGOW_HASKELL__ > 708
pattern $bSpecific :: SpecificCat k α β -> k α β
$mSpecific :: forall r (k :: * -> * -> *) α β.
CRCategory k =>
k α β -> (SpecificCat k α β -> r) -> (Void# -> r) -> r
Specific f <- (match_concrete -> Just f) where
Specific SpecificCat k α β
f = SpecificCat k α β -> k α β
forall (k :: * -> * -> *) α β.
CRCategory k =>
SpecificCat k α β -> k α β
fromSpecific SpecificCat k α β
f
pattern $bId :: k α β
$mId :: forall r (k :: * -> * -> *) α β.
CRCategory k =>
k α β -> ((β ~ α, Object k α) => r) -> (Void# -> r) -> r
Id <- (match_id -> IsId) where
Id = k α β
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
pattern g$m:<<< :: forall r (k :: * -> * -> *) α β.
CRCategory k =>
k α β
-> (forall β1. Object k β1 => k β1 β -> k α β1 -> r)
-> (Void# -> r)
-> r
:<<<f <- (match_compose -> IsCompo f g)
pattern f$m:>>> :: forall r (k :: * -> * -> *) α β.
CRCategory k =>
k α β
-> (forall β1. Object k β1 => k α β1 -> k β1 β -> r)
-> (Void# -> r)
-> r
:>>>g <- (match_compose -> IsCompo f g)
#endif
instance Cartesian k => CRCategory (ReCartesian k) where
type SpecificCat (ReCartesian k) = k
fromSpecific :: SpecificCat (ReCartesian k) α β -> ReCartesian k α β
fromSpecific = SpecificCat (ReCartesian k) α β -> ReCartesian k α β
forall (k :: * -> * -> *) α β. k α β -> ReCartesian k α β
ReCartesian
match_concrete :: ReCartesian k α β -> Maybe (SpecificCat (ReCartesian k) α β)
match_concrete (ReCartesian k α β
f) = k α β -> Maybe (k α β)
forall a. a -> Maybe a
Just k α β
f
match_concrete ReCartesian k α β
_ = Maybe (SpecificCat (ReCartesian k) α β)
forall a. Maybe a
Nothing
match_id :: ReCartesian k α β -> IdPattern (ReCartesian k) α β
match_id (ReCartesian k α β
CartesianId) = IdPattern (ReCartesian k) α β
forall (k :: * -> * -> *) α. Object k α => IdPattern k α α
IsId
match_id ReCartesian k α β
_ = IdPattern (ReCartesian k) α β
forall (k :: * -> * -> *) α β. IdPattern k α β
NotId
match_compose :: ReCartesian k α β -> CompoPattern (ReCartesian k) α β
match_compose (CartesianCompo ReCartesian k α β
f ReCartesian k β β
g) = ReCartesian k α β
-> ReCartesian k β β -> CompoPattern (ReCartesian k) α β
forall (k :: * -> * -> *) β α γ.
Object k β =>
k α β -> k β γ -> CompoPattern k α γ
IsCompo ReCartesian k α β
f ReCartesian k β β
g
match_compose ReCartesian k α β
_ = CompoPattern (ReCartesian k) α β
forall (k :: * -> * -> *) α β. CompoPattern k α β
NotCompo
data SwapPattern k α β where
IsSwap :: (ObjectPair k α β, ObjectPair k β α)
=> SwapPattern k (α,β) (β,α)
NotSwap :: SwapPattern k α β
data AttachUnitPattern k α β where
IsAttachUnit :: (Object k α, UnitObject k ~ u, ObjectPair k α u)
=> AttachUnitPattern k α (α,u)
NotAttachUnit :: AttachUnitPattern k α β
data DetachUnitPattern k α β where
IsDetachUnit :: (Object k α, UnitObject k ~ u, ObjectPair k α u)
=> DetachUnitPattern k (α,u) α
NotDetachUnit :: DetachUnitPattern k α β
data RegroupPattern k α β where
IsRegroup :: ( ObjectPair k α β, ObjectPair k β γ
, ObjectPair k α (β,γ), ObjectPair k (α,β) γ )
=> RegroupPattern k (α,(β,γ)) ((α,β),γ)
NotRegroup :: RegroupPattern k α β
data Regroup'Pattern k α β where
IsRegroup' :: ( ObjectPair k α β, ObjectPair k β γ
, ObjectPair k α (β,γ), ObjectPair k (α,β) γ )
=> Regroup'Pattern k ((α,β),γ) (α,(β,γ))
NotRegroup' :: Regroup'Pattern k α β
class CRCategory k => CRCartesian k where
match_swap :: k α β -> SwapPattern k α β
match_attachUnit :: k α β -> AttachUnitPattern k α β
match_detachUnit :: k α β -> DetachUnitPattern k α β
match_regroup :: k α β -> RegroupPattern k α β
match_regroup' :: k α β -> Regroup'Pattern k α β
instance Cartesian k => CRCartesian (ReCartesian k) where
match_swap :: ReCartesian k α β -> SwapPattern (ReCartesian k) α β
match_swap (ReCartesian k α β
CartesianSwap) = SwapPattern (ReCartesian k) α β
forall (k :: * -> * -> *) α β.
(ObjectPair k α β, ObjectPair k β α) =>
SwapPattern k (α, β) (β, α)
IsSwap
match_swap ReCartesian k α β
_ = SwapPattern (ReCartesian k) α β
forall (k :: * -> * -> *) α β. SwapPattern k α β
NotSwap
match_attachUnit :: ReCartesian k α β -> AttachUnitPattern (ReCartesian k) α β
match_attachUnit (ReCartesian k α β
CartesianAttachUnit) = AttachUnitPattern (ReCartesian k) α β
forall (k :: * -> * -> *) α u.
(Object k α, UnitObject k ~ u, ObjectPair k α u) =>
AttachUnitPattern k α (α, u)
IsAttachUnit
match_attachUnit ReCartesian k α β
_ = AttachUnitPattern (ReCartesian k) α β
forall (k :: * -> * -> *) α β. AttachUnitPattern k α β
NotAttachUnit
match_detachUnit :: ReCartesian k α β -> DetachUnitPattern (ReCartesian k) α β
match_detachUnit (ReCartesian k α β
CartesianDetachUnit) = DetachUnitPattern (ReCartesian k) α β
forall (k :: * -> * -> *) α u.
(Object k α, UnitObject k ~ u, ObjectPair k α u) =>
DetachUnitPattern k (α, u) α
IsDetachUnit
match_detachUnit ReCartesian k α β
_ = DetachUnitPattern (ReCartesian k) α β
forall (k :: * -> * -> *) α β. DetachUnitPattern k α β
NotDetachUnit
match_regroup :: ReCartesian k α β -> RegroupPattern (ReCartesian k) α β
match_regroup (ReCartesian k α β
CartesianRegroup) = RegroupPattern (ReCartesian k) α β
forall (k :: * -> * -> *) α β γ.
(ObjectPair k α β, ObjectPair k β γ, ObjectPair k α (β, γ),
ObjectPair k (α, β) γ) =>
RegroupPattern k (α, (β, γ)) ((α, β), γ)
IsRegroup
match_regroup ReCartesian k α β
_ = RegroupPattern (ReCartesian k) α β
forall (k :: * -> * -> *) α β. RegroupPattern k α β
NotRegroup
match_regroup' :: ReCartesian k α β -> Regroup'Pattern (ReCartesian k) α β
match_regroup' (ReCartesian k α β
CartesianRegroup_) = Regroup'Pattern (ReCartesian k) α β
forall (k :: * -> * -> *) α β γ.
(ObjectPair k α β, ObjectPair k β γ, ObjectPair k α (β, γ),
ObjectPair k (α, β) γ) =>
Regroup'Pattern k ((α, β), γ) (α, (β, γ))
IsRegroup'
match_regroup' ReCartesian k α β
_ = Regroup'Pattern (ReCartesian k) α β
forall (k :: * -> * -> *) α β. Regroup'Pattern k α β
NotRegroup'
#if __GLASGOW_HASKELL__ > 708
pattern $mSwap :: forall r (k :: * -> * -> *) α β.
CRCartesian k =>
k α β
-> (forall α1 β1.
(α ~ (α1, β1), β ~ (β1, α1), ObjectPair k α1 β1,
ObjectPair k β1 α1) =>
r)
-> (Void# -> r)
-> r
Swap <- (match_swap -> IsSwap)
pattern $mAttachUnit :: forall r (k :: * -> * -> *) α β.
CRCartesian k =>
k α β
-> (forall u.
(β ~ (α, u), UnitObject k ~ u, ObjectPair k α u) =>
r)
-> (Void# -> r)
-> r
AttachUnit <- (match_attachUnit -> IsAttachUnit)
pattern $mDetachUnit :: forall r (k :: * -> * -> *) α β.
CRCartesian k =>
k α β
-> (forall u.
(α ~ (β, u), UnitObject k ~ u, ObjectPair k β u) =>
r)
-> (Void# -> r)
-> r
DetachUnit <- (match_detachUnit -> IsDetachUnit)
pattern $mRegroup :: forall r (k :: * -> * -> *) α β.
CRCartesian k =>
k α β
-> (forall α1 β1 γ.
(α ~ (α1, (β1, γ)), β ~ ((α1, β1), γ), ObjectPair k α1 β1,
ObjectPair k β1 γ, ObjectPair k α1 (β1, γ),
ObjectPair k (α1, β1) γ) =>
r)
-> (Void# -> r)
-> r
Regroup <- (match_regroup -> IsRegroup)
pattern $mRegroup' :: forall r (k :: * -> * -> *) α β.
CRCartesian k =>
k α β
-> (forall α1 β1 γ.
(α ~ ((α1, β1), γ), β ~ (α1, (β1, γ)), ObjectPair k α1 β1,
ObjectPair k β1 γ, ObjectPair k α1 (β1, γ),
ObjectPair k (α1, β1) γ) =>
r)
-> (Void# -> r)
-> r
Regroup' <- (match_regroup' -> IsRegroup')
#endif
#if __GLASGOW_HASKELL__ > 708
infixr 3 :***
#endif
instance Morphism k => CRCategory (ReMorphism k) where
type SpecificCat (ReMorphism k) = k
fromSpecific :: SpecificCat (ReMorphism k) α β -> ReMorphism k α β
fromSpecific = SpecificCat (ReMorphism k) α β -> ReMorphism k α β
forall (k :: * -> * -> *) α β. k α β -> ReMorphism k α β
ReMorphism
match_concrete :: ReMorphism k α β -> Maybe (SpecificCat (ReMorphism k) α β)
match_concrete (ReMorphism k α β
f) = k α β -> Maybe (k α β)
forall a. a -> Maybe a
Just k α β
f
match_concrete ReMorphism k α β
_ = Maybe (SpecificCat (ReMorphism k) α β)
forall a. Maybe a
Nothing
match_id :: ReMorphism k α β -> IdPattern (ReMorphism k) α β
match_id (ReMorphism k α β
MorphismId) = IdPattern (ReMorphism k) α β
forall (k :: * -> * -> *) α. Object k α => IdPattern k α α
IsId
match_id ReMorphism k α β
_ = IdPattern (ReMorphism k) α β
forall (k :: * -> * -> *) α β. IdPattern k α β
NotId
match_compose :: ReMorphism k α β -> CompoPattern (ReMorphism k) α β
match_compose (MorphismCompo ReMorphism k α β
f ReMorphism k β β
g) = ReMorphism k α β
-> ReMorphism k β β -> CompoPattern (ReMorphism k) α β
forall (k :: * -> * -> *) β α γ.
Object k β =>
k α β -> k β γ -> CompoPattern k α γ
IsCompo ReMorphism k α β
f ReMorphism k β β
g
match_compose ReMorphism k α β
_ = CompoPattern (ReMorphism k) α β
forall (k :: * -> * -> *) α β. CompoPattern k α β
NotCompo
instance Morphism k => CRCartesian (ReMorphism k) where
match_swap :: ReMorphism k α β -> SwapPattern (ReMorphism k) α β
match_swap (ReMorphism k α β
MorphismSwap) = SwapPattern (ReMorphism k) α β
forall (k :: * -> * -> *) α β.
(ObjectPair k α β, ObjectPair k β α) =>
SwapPattern k (α, β) (β, α)
IsSwap
match_swap ReMorphism k α β
_ = SwapPattern (ReMorphism k) α β
forall (k :: * -> * -> *) α β. SwapPattern k α β
NotSwap
match_attachUnit :: ReMorphism k α β -> AttachUnitPattern (ReMorphism k) α β
match_attachUnit (ReMorphism k α β
MorphismAttachUnit) = AttachUnitPattern (ReMorphism k) α β
forall (k :: * -> * -> *) α u.
(Object k α, UnitObject k ~ u, ObjectPair k α u) =>
AttachUnitPattern k α (α, u)
IsAttachUnit
match_attachUnit ReMorphism k α β
_ = AttachUnitPattern (ReMorphism k) α β
forall (k :: * -> * -> *) α β. AttachUnitPattern k α β
NotAttachUnit
match_detachUnit :: ReMorphism k α β -> DetachUnitPattern (ReMorphism k) α β
match_detachUnit (ReMorphism k α β
MorphismDetachUnit) = DetachUnitPattern (ReMorphism k) α β
forall (k :: * -> * -> *) α u.
(Object k α, UnitObject k ~ u, ObjectPair k α u) =>
DetachUnitPattern k (α, u) α
IsDetachUnit
match_detachUnit ReMorphism k α β
_ = DetachUnitPattern (ReMorphism k) α β
forall (k :: * -> * -> *) α β. DetachUnitPattern k α β
NotDetachUnit
match_regroup :: ReMorphism k α β -> RegroupPattern (ReMorphism k) α β
match_regroup (ReMorphism k α β
MorphismRegroup) = RegroupPattern (ReMorphism k) α β
forall (k :: * -> * -> *) α β γ.
(ObjectPair k α β, ObjectPair k β γ, ObjectPair k α (β, γ),
ObjectPair k (α, β) γ) =>
RegroupPattern k (α, (β, γ)) ((α, β), γ)
IsRegroup
match_regroup ReMorphism k α β
_ = RegroupPattern (ReMorphism k) α β
forall (k :: * -> * -> *) α β. RegroupPattern k α β
NotRegroup
match_regroup' :: ReMorphism k α β -> Regroup'Pattern (ReMorphism k) α β
match_regroup' (ReMorphism k α β
MorphismRegroup_) = Regroup'Pattern (ReMorphism k) α β
forall (k :: * -> * -> *) α β γ.
(ObjectPair k α β, ObjectPair k β γ, ObjectPair k α (β, γ),
ObjectPair k (α, β) γ) =>
Regroup'Pattern k ((α, β), γ) (α, (β, γ))
IsRegroup'
match_regroup' ReMorphism k α β
_ = Regroup'Pattern (ReMorphism k) α β
forall (k :: * -> * -> *) α β. Regroup'Pattern k α β
NotRegroup'
data ParPattern k α β where
IsPar :: (ObjectPair k α γ, ObjectPair k β δ)
=> k α β -> k γ δ -> ParPattern k (α,γ) (β,δ)
NotPar :: ParPattern k α β
class CRCartesian k => CRMorphism k where
match_par :: k α β -> ParPattern k α β
instance Morphism k => CRMorphism (ReMorphism k) where
match_par :: ReMorphism k α β -> ParPattern (ReMorphism k) α β
match_par (MorphismPar ReMorphism k α β
f ReMorphism k γ δ
g) = ReMorphism k α β
-> ReMorphism k γ δ -> ParPattern (ReMorphism k) (α, γ) (β, δ)
forall (k :: * -> * -> *) α γ β δ.
(ObjectPair k α γ, ObjectPair k β δ) =>
k α β -> k γ δ -> ParPattern k (α, γ) (β, δ)
IsPar ReMorphism k α β
f ReMorphism k γ δ
g
match_par ReMorphism k α β
_ = ParPattern (ReMorphism k) α β
forall (k :: * -> * -> *) α β. ParPattern k α β
NotPar
#if __GLASGOW_HASKELL__ > 708
pattern f$m:*** :: forall r (k :: * -> * -> *) α β.
CRMorphism k =>
k α β
-> (forall α1 γ β1 δ.
(α ~ (α1, γ), β ~ (β1, δ), ObjectPair k α1 γ, ObjectPair k β1 δ) =>
k α1 β1 -> k γ δ -> r)
-> (Void# -> r)
-> r
:***g <- (match_par -> IsPar f g)
#endif
#if __GLASGOW_HASKELL__ > 708
infixr 3 :&&&
#endif
instance PreArrow k => CRCategory (RePreArrow k) where
type SpecificCat (RePreArrow k) = k
fromSpecific :: SpecificCat (RePreArrow k) α β -> RePreArrow k α β
fromSpecific = SpecificCat (RePreArrow k) α β -> RePreArrow k α β
forall (k :: * -> * -> *) α β. k α β -> RePreArrow k α β
RePreArrow
match_concrete :: RePreArrow k α β -> Maybe (SpecificCat (RePreArrow k) α β)
match_concrete (RePreArrow k α β
f) = k α β -> Maybe (k α β)
forall a. a -> Maybe a
Just k α β
f
match_concrete RePreArrow k α β
_ = Maybe (SpecificCat (RePreArrow k) α β)
forall a. Maybe a
Nothing
match_id :: RePreArrow k α β -> IdPattern (RePreArrow k) α β
match_id (RePreArrow k α β
PreArrowId) = IdPattern (RePreArrow k) α β
forall (k :: * -> * -> *) α. Object k α => IdPattern k α α
IsId
match_id RePreArrow k α β
_ = IdPattern (RePreArrow k) α β
forall (k :: * -> * -> *) α β. IdPattern k α β
NotId
match_compose :: RePreArrow k α β -> CompoPattern (RePreArrow k) α β
match_compose (PreArrowCompo RePreArrow k α β
f RePreArrow k β β
g) = RePreArrow k α β
-> RePreArrow k β β -> CompoPattern (RePreArrow k) α β
forall (k :: * -> * -> *) β α γ.
Object k β =>
k α β -> k β γ -> CompoPattern k α γ
IsCompo RePreArrow k α β
f RePreArrow k β β
g
match_compose RePreArrow k α β
_ = CompoPattern (RePreArrow k) α β
forall (k :: * -> * -> *) α β. CompoPattern k α β
NotCompo
instance PreArrow k => CRCartesian (RePreArrow k) where
match_swap :: RePreArrow k α β -> SwapPattern (RePreArrow k) α β
match_swap (RePreArrow k α β
PreArrowSwap) = SwapPattern (RePreArrow k) α β
forall (k :: * -> * -> *) α β.
(ObjectPair k α β, ObjectPair k β α) =>
SwapPattern k (α, β) (β, α)
IsSwap
match_swap RePreArrow k α β
_ = SwapPattern (RePreArrow k) α β
forall (k :: * -> * -> *) α β. SwapPattern k α β
NotSwap
match_attachUnit :: RePreArrow k α β -> AttachUnitPattern (RePreArrow k) α β
match_attachUnit (RePreArrow k α β
PreArrowAttachUnit) = AttachUnitPattern (RePreArrow k) α β
forall (k :: * -> * -> *) α u.
(Object k α, UnitObject k ~ u, ObjectPair k α u) =>
AttachUnitPattern k α (α, u)
IsAttachUnit
match_attachUnit RePreArrow k α β
_ = AttachUnitPattern (RePreArrow k) α β
forall (k :: * -> * -> *) α β. AttachUnitPattern k α β
NotAttachUnit
match_detachUnit :: RePreArrow k α β -> DetachUnitPattern (RePreArrow k) α β
match_detachUnit (RePreArrow k α β
PreArrowDetachUnit) = DetachUnitPattern (RePreArrow k) α β
forall (k :: * -> * -> *) α u.
(Object k α, UnitObject k ~ u, ObjectPair k α u) =>
DetachUnitPattern k (α, u) α
IsDetachUnit
match_detachUnit RePreArrow k α β
_ = DetachUnitPattern (RePreArrow k) α β
forall (k :: * -> * -> *) α β. DetachUnitPattern k α β
NotDetachUnit
match_regroup :: RePreArrow k α β -> RegroupPattern (RePreArrow k) α β
match_regroup (RePreArrow k α β
PreArrowRegroup) = RegroupPattern (RePreArrow k) α β
forall (k :: * -> * -> *) α β γ.
(ObjectPair k α β, ObjectPair k β γ, ObjectPair k α (β, γ),
ObjectPair k (α, β) γ) =>
RegroupPattern k (α, (β, γ)) ((α, β), γ)
IsRegroup
match_regroup RePreArrow k α β
_ = RegroupPattern (RePreArrow k) α β
forall (k :: * -> * -> *) α β. RegroupPattern k α β
NotRegroup
match_regroup' :: RePreArrow k α β -> Regroup'Pattern (RePreArrow k) α β
match_regroup' (RePreArrow k α β
PreArrowRegroup_) = Regroup'Pattern (RePreArrow k) α β
forall (k :: * -> * -> *) α β γ.
(ObjectPair k α β, ObjectPair k β γ, ObjectPair k α (β, γ),
ObjectPair k (α, β) γ) =>
Regroup'Pattern k ((α, β), γ) (α, (β, γ))
IsRegroup'
match_regroup' RePreArrow k α β
_ = Regroup'Pattern (RePreArrow k) α β
forall (k :: * -> * -> *) α β. Regroup'Pattern k α β
NotRegroup'
instance PreArrow k => CRMorphism (RePreArrow k) where
match_par :: RePreArrow k α β -> ParPattern (RePreArrow k) α β
match_par (PreArrowPar RePreArrow k α β
f RePreArrow k γ δ
g) = RePreArrow k α β
-> RePreArrow k γ δ -> ParPattern (RePreArrow k) (α, γ) (β, δ)
forall (k :: * -> * -> *) α γ β δ.
(ObjectPair k α γ, ObjectPair k β δ) =>
k α β -> k γ δ -> ParPattern k (α, γ) (β, δ)
IsPar RePreArrow k α β
f RePreArrow k γ δ
g
match_par RePreArrow k α β
_ = ParPattern (RePreArrow k) α β
forall (k :: * -> * -> *) α β. ParPattern k α β
NotPar
data FanPattern k α β where
IsFan :: (Object k α, ObjectPair k β γ)
=> k α β -> k α γ -> FanPattern k α (β,γ)
NotFan :: FanPattern k α β
data FstPattern k α β where
IsFst :: (ObjectPair k α β)
=> FstPattern k (α,β) α
NotFst :: FstPattern k α β
data SndPattern k α β where
IsSnd :: (ObjectPair k α β)
=> SndPattern k (α,β) β
NotSnd :: SndPattern k α β
data TerminalPattern k α β where
IsTerminal :: (Object k α, UnitObject k ~ u)
=> TerminalPattern k α u
NotTerminal :: TerminalPattern k α β
class CRCartesian k => CRPreArrow k where
match_fan :: k α β -> FanPattern k α β
match_fst :: k α β -> FstPattern k α β
match_snd :: k α β -> SndPattern k α β
match_terminal :: k α β -> TerminalPattern k α β
#if __GLASGOW_HASKELL__ > 708
pattern f$m:&&& :: forall r (k :: * -> * -> *) α β.
CRPreArrow k =>
k α β
-> (forall β1 γ.
(β ~ (β1, γ), Object k α, ObjectPair k β1 γ) =>
k α β1 -> k α γ -> r)
-> (Void# -> r)
-> r
:&&&g <- (match_fan -> IsFan f g)
pattern $mFst :: forall r (k :: * -> * -> *) α β.
CRPreArrow k =>
k α β
-> (forall β1. (α ~ (β, β1), ObjectPair k β β1) => r)
-> (Void# -> r)
-> r
Fst <- (match_fst -> IsFst)
pattern $mSnd :: forall r (k :: * -> * -> *) α β.
CRPreArrow k =>
k α β
-> (forall α1. (α ~ (α1, β), ObjectPair k α1 β) => r)
-> (Void# -> r)
-> r
Snd <- (match_snd -> IsSnd)
pattern $mTerminal :: forall r (k :: * -> * -> *) α β.
CRPreArrow k =>
k α β -> ((Object k α, UnitObject k ~ β) => r) -> (Void# -> r) -> r
Terminal <- (match_terminal -> IsTerminal)
#endif
instance PreArrow k => CRPreArrow (RePreArrow k) where
match_fan :: RePreArrow k α β -> FanPattern (RePreArrow k) α β
match_fan (PreArrowFanout RePreArrow k α β
f RePreArrow k α γ
g) = RePreArrow k α β
-> RePreArrow k α γ -> FanPattern (RePreArrow k) α (β, γ)
forall (k :: * -> * -> *) α β γ.
(Object k α, ObjectPair k β γ) =>
k α β -> k α γ -> FanPattern k α (β, γ)
IsFan RePreArrow k α β
f RePreArrow k α γ
g
match_fan RePreArrow k α β
_ = FanPattern (RePreArrow k) α β
forall (k :: * -> * -> *) α β. FanPattern k α β
NotFan
match_fst :: RePreArrow k α β -> FstPattern (RePreArrow k) α β
match_fst RePreArrow k α β
PreArrowFst = FstPattern (RePreArrow k) α β
forall (k :: * -> * -> *) α β.
ObjectPair k α β =>
FstPattern k (α, β) α
IsFst
match_fst RePreArrow k α β
_ = FstPattern (RePreArrow k) α β
forall (k :: * -> * -> *) α β. FstPattern k α β
NotFst
match_snd :: RePreArrow k α β -> SndPattern (RePreArrow k) α β
match_snd RePreArrow k α β
PreArrowSnd = SndPattern (RePreArrow k) α β
forall (k :: * -> * -> *) α β.
ObjectPair k α β =>
SndPattern k (α, β) β
IsSnd
match_snd RePreArrow k α β
_ = SndPattern (RePreArrow k) α β
forall (k :: * -> * -> *) α β. SndPattern k α β
NotSnd
match_terminal :: RePreArrow k α β -> TerminalPattern (RePreArrow k) α β
match_terminal RePreArrow k α β
PreArrowTerminal = TerminalPattern (RePreArrow k) α β
forall (k :: * -> * -> *) α u.
(Object k α, UnitObject k ~ u) =>
TerminalPattern k α u
IsTerminal
match_terminal RePreArrow k α β
_ = TerminalPattern (RePreArrow k) α β
forall (k :: * -> * -> *) α β. TerminalPattern k α β
NotTerminal
instance WellPointed k => CRCategory (ReWellPointed k) where
type SpecificCat (ReWellPointed k) = k
fromSpecific :: SpecificCat (ReWellPointed k) α β -> ReWellPointed k α β
fromSpecific = SpecificCat (ReWellPointed k) α β -> ReWellPointed k α β
forall (k :: * -> * -> *) α β. k α β -> ReWellPointed k α β
ReWellPointed
match_concrete :: ReWellPointed k α β -> Maybe (SpecificCat (ReWellPointed k) α β)
match_concrete (ReWellPointed k α β
f) = k α β -> Maybe (k α β)
forall a. a -> Maybe a
Just k α β
f
match_concrete ReWellPointed k α β
_ = Maybe (SpecificCat (ReWellPointed k) α β)
forall a. Maybe a
Nothing
match_id :: ReWellPointed k α β -> IdPattern (ReWellPointed k) α β
match_id (ReWellPointed k α β
WellPointedId) = IdPattern (ReWellPointed k) α β
forall (k :: * -> * -> *) α. Object k α => IdPattern k α α
IsId
match_id ReWellPointed k α β
_ = IdPattern (ReWellPointed k) α β
forall (k :: * -> * -> *) α β. IdPattern k α β
NotId
match_compose :: ReWellPointed k α β -> CompoPattern (ReWellPointed k) α β
match_compose (WellPointedCompo ReWellPointed k α β
f ReWellPointed k β β
g) = ReWellPointed k α β
-> ReWellPointed k β β -> CompoPattern (ReWellPointed k) α β
forall (k :: * -> * -> *) β α γ.
Object k β =>
k α β -> k β γ -> CompoPattern k α γ
IsCompo ReWellPointed k α β
f ReWellPointed k β β
g
match_compose ReWellPointed k α β
_ = CompoPattern (ReWellPointed k) α β
forall (k :: * -> * -> *) α β. CompoPattern k α β
NotCompo
instance WellPointed k => CRCartesian (ReWellPointed k) where
match_swap :: ReWellPointed k α β -> SwapPattern (ReWellPointed k) α β
match_swap (ReWellPointed k α β
WellPointedSwap) = SwapPattern (ReWellPointed k) α β
forall (k :: * -> * -> *) α β.
(ObjectPair k α β, ObjectPair k β α) =>
SwapPattern k (α, β) (β, α)
IsSwap
match_swap ReWellPointed k α β
_ = SwapPattern (ReWellPointed k) α β
forall (k :: * -> * -> *) α β. SwapPattern k α β
NotSwap
match_attachUnit :: ReWellPointed k α β -> AttachUnitPattern (ReWellPointed k) α β
match_attachUnit (ReWellPointed k α β
WellPointedAttachUnit) = AttachUnitPattern (ReWellPointed k) α β
forall (k :: * -> * -> *) α u.
(Object k α, UnitObject k ~ u, ObjectPair k α u) =>
AttachUnitPattern k α (α, u)
IsAttachUnit
match_attachUnit ReWellPointed k α β
_ = AttachUnitPattern (ReWellPointed k) α β
forall (k :: * -> * -> *) α β. AttachUnitPattern k α β
NotAttachUnit
match_detachUnit :: ReWellPointed k α β -> DetachUnitPattern (ReWellPointed k) α β
match_detachUnit (ReWellPointed k α β
WellPointedDetachUnit) = DetachUnitPattern (ReWellPointed k) α β
forall (k :: * -> * -> *) α u.
(Object k α, UnitObject k ~ u, ObjectPair k α u) =>
DetachUnitPattern k (α, u) α
IsDetachUnit
match_detachUnit ReWellPointed k α β
_ = DetachUnitPattern (ReWellPointed k) α β
forall (k :: * -> * -> *) α β. DetachUnitPattern k α β
NotDetachUnit
match_regroup :: ReWellPointed k α β -> RegroupPattern (ReWellPointed k) α β
match_regroup (ReWellPointed k α β
WellPointedRegroup) = RegroupPattern (ReWellPointed k) α β
forall (k :: * -> * -> *) α β γ.
(ObjectPair k α β, ObjectPair k β γ, ObjectPair k α (β, γ),
ObjectPair k (α, β) γ) =>
RegroupPattern k (α, (β, γ)) ((α, β), γ)
IsRegroup
match_regroup ReWellPointed k α β
_ = RegroupPattern (ReWellPointed k) α β
forall (k :: * -> * -> *) α β. RegroupPattern k α β
NotRegroup
match_regroup' :: ReWellPointed k α β -> Regroup'Pattern (ReWellPointed k) α β
match_regroup' (ReWellPointed k α β
WellPointedRegroup_) = Regroup'Pattern (ReWellPointed k) α β
forall (k :: * -> * -> *) α β γ.
(ObjectPair k α β, ObjectPair k β γ, ObjectPair k α (β, γ),
ObjectPair k (α, β) γ) =>
Regroup'Pattern k ((α, β), γ) (α, (β, γ))
IsRegroup'
match_regroup' ReWellPointed k α β
_ = Regroup'Pattern (ReWellPointed k) α β
forall (k :: * -> * -> *) α β. Regroup'Pattern k α β
NotRegroup'
instance WellPointed k => CRMorphism (ReWellPointed k) where
match_par :: ReWellPointed k α β -> ParPattern (ReWellPointed k) α β
match_par (WellPointedPar ReWellPointed k α β
f ReWellPointed k γ δ
g) = ReWellPointed k α β
-> ReWellPointed k γ δ
-> ParPattern (ReWellPointed k) (α, γ) (β, δ)
forall (k :: * -> * -> *) α γ β δ.
(ObjectPair k α γ, ObjectPair k β δ) =>
k α β -> k γ δ -> ParPattern k (α, γ) (β, δ)
IsPar ReWellPointed k α β
f ReWellPointed k γ δ
g
match_par ReWellPointed k α β
_ = ParPattern (ReWellPointed k) α β
forall (k :: * -> * -> *) α β. ParPattern k α β
NotPar
instance WellPointed k => CRPreArrow (ReWellPointed k) where
match_fan :: ReWellPointed k α β -> FanPattern (ReWellPointed k) α β
match_fan (WellPointedFanout ReWellPointed k α β
f ReWellPointed k α γ
g) = ReWellPointed k α β
-> ReWellPointed k α γ -> FanPattern (ReWellPointed k) α (β, γ)
forall (k :: * -> * -> *) α β γ.
(Object k α, ObjectPair k β γ) =>
k α β -> k α γ -> FanPattern k α (β, γ)
IsFan ReWellPointed k α β
f ReWellPointed k α γ
g
match_fan ReWellPointed k α β
_ = FanPattern (ReWellPointed k) α β
forall (k :: * -> * -> *) α β. FanPattern k α β
NotFan
match_fst :: ReWellPointed k α β -> FstPattern (ReWellPointed k) α β
match_fst ReWellPointed k α β
WellPointedFst = FstPattern (ReWellPointed k) α β
forall (k :: * -> * -> *) α β.
ObjectPair k α β =>
FstPattern k (α, β) α
IsFst
match_fst ReWellPointed k α β
_ = FstPattern (ReWellPointed k) α β
forall (k :: * -> * -> *) α β. FstPattern k α β
NotFst
match_snd :: ReWellPointed k α β -> SndPattern (ReWellPointed k) α β
match_snd ReWellPointed k α β
WellPointedSnd = SndPattern (ReWellPointed k) α β
forall (k :: * -> * -> *) α β.
ObjectPair k α β =>
SndPattern k (α, β) β
IsSnd
match_snd ReWellPointed k α β
_ = SndPattern (ReWellPointed k) α β
forall (k :: * -> * -> *) α β. SndPattern k α β
NotSnd
match_terminal :: ReWellPointed k α β -> TerminalPattern (ReWellPointed k) α β
match_terminal ReWellPointed k α β
WellPointedTerminal = TerminalPattern (ReWellPointed k) α β
forall (k :: * -> * -> *) α u.
(Object k α, UnitObject k ~ u) =>
TerminalPattern k α u
IsTerminal
match_terminal ReWellPointed k α β
_ = TerminalPattern (ReWellPointed k) α β
forall (k :: * -> * -> *) α β. TerminalPattern k α β
NotTerminal
data ConstPattern k α β where
IsConst :: (Object k α, Object k β)
=> β -> ConstPattern k α β
NotConst :: ConstPattern k α β
class CRPreArrow k => CRWellPointed k where
match_const :: k α β -> ConstPattern k α β
#if __GLASGOW_HASKELL__ > 708
pattern $mConst :: forall r (k :: * -> * -> *) α β.
CRWellPointed k =>
k α β -> ((Object k α, Object k β) => β -> r) -> (Void# -> r) -> r
Const c <- (match_const -> IsConst c)
#endif
instance WellPointed k => CRWellPointed (ReWellPointed k) where
match_const :: ReWellPointed k α β -> ConstPattern (ReWellPointed k) α β
match_const (WellPointedConst β
c) = β -> ConstPattern (ReWellPointed k) α β
forall (k :: * -> * -> *) α β.
(Object k α, Object k β) =>
β -> ConstPattern k α β
IsConst β
c
match_const ReWellPointed k α β
_ = ConstPattern (ReWellPointed k) α β
forall (k :: * -> * -> *) α β. ConstPattern k α β
NotConst