-- |
-- Module      :  Control.Category.Constrained.Reified.PolyPattern
-- Copyright   :  (c) 2016 Justus Sagemüller
-- License     :  GPL v3 (see COPYING)
-- Maintainer  :  (@) jsag $ hvl.no
-- 
-- 
-- Pattern synonyms which allow you to deconstruct the various types
-- in "Control.Category.Constrained.Reified" in a uniform way.
-- 
-- This kind of polymorphic pattern (with @ViewPatterns@) doesn't
-- seem to work prior to GHC-7.10, so if you have base<4.8 these
-- synonyms aren't available.

{-# 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 synonyms (GHC>=7.10)
      -- ** Category
         pattern Specific, pattern Id, pattern (:<<<), pattern (:>>>)
      -- ** Cartesian
       , pattern Swap
       , pattern AttachUnit, pattern DetachUnit
       , pattern Regroup, pattern Regroup'
      -- ** Morphism
       , pattern (:***)
      -- ** Pre-arrow
       , pattern (:&&&), pattern Fst, pattern Snd, pattern Terminal
      -- ** Well-pointed
       , pattern Const,
#endif
      -- * Deconstruction-classes
         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 :: forall α β. SpecificCat (ReCategory k) α β -> ReCategory k α β
fromSpecific = forall (k :: * -> * -> *) α β. k α β -> ReCategory k α β
ReCategory
  match_concrete :: forall α β.
ReCategory k α β -> Maybe (SpecificCat (ReCategory k) α β)
match_concrete (ReCategory k α β
f) = forall a. a -> Maybe a
Just k α β
f
  match_concrete ReCategory k α β
_ = forall a. Maybe a
Nothing
  match_id :: forall α β. ReCategory k α β -> IdPattern (ReCategory k) α β
match_id ReCategory k α β
CategoryId = forall (k :: * -> * -> *) α. Object k α => IdPattern k α α
IsId
  match_id ReCategory k α β
_ = forall (k :: * -> * -> *) α β. IdPattern k α β
NotId
  match_compose :: forall α β. ReCategory k α β -> CompoPattern (ReCategory k) α β
match_compose (CategoryCompo ReCategory k α β
f ReCategory k β β
g) = forall (k :: * -> * -> *) α α γ.
Object k α =>
k α α -> k α γ -> CompoPattern k α γ
IsCompo ReCategory k α β
f ReCategory k β β
g
  match_compose ReCategory k α β
_ = forall (k :: * -> * -> *) α β. CompoPattern k α β
NotCompo

#if __GLASGOW_HASKELL__ > 708
pattern $bSpecific :: forall {k :: * -> * -> *} {α} {β}.
CRCategory k =>
SpecificCat k α β -> k α β
$mSpecific :: forall {r} {k :: * -> * -> *} {α} {β}.
CRCategory k =>
k α β -> (SpecificCat k α β -> r) -> ((# #) -> r) -> r
Specific f <- (match_concrete -> Just f) where
  Specific SpecificCat k α β
f = forall (k :: * -> * -> *) α β.
CRCategory k =>
SpecificCat k α β -> k α β
fromSpecific SpecificCat k α β
f
pattern $bId :: forall {k :: * -> * -> *} {α} {β}.
(CRCategory k, β ~ α, Object k α) =>
k α β
$mId :: forall {r} {k :: * -> * -> *} {α} {β}.
CRCategory k =>
k α β -> ((β ~ α, Object k α) => r) -> ((# #) -> r) -> r
Id <- (match_id -> IsId) where
  Id = 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)
-> ((# #) -> 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)
-> ((# #) -> r)
-> r
:>>>g <- (match_compose -> IsCompo f g)
#endif
  
instance Cartesian k => CRCategory (ReCartesian k) where
  type SpecificCat (ReCartesian k) = k
  fromSpecific :: forall α β. SpecificCat (ReCartesian k) α β -> ReCartesian k α β
fromSpecific = forall (k :: * -> * -> *) α β. k α β -> ReCartesian k α β
ReCartesian
  match_concrete :: forall α β.
ReCartesian k α β -> Maybe (SpecificCat (ReCartesian k) α β)
match_concrete (ReCartesian k α β
f) = forall a. a -> Maybe a
Just k α β
f
  match_concrete ReCartesian k α β
_ = forall a. Maybe a
Nothing
  match_id :: forall α β. ReCartesian k α β -> IdPattern (ReCartesian k) α β
match_id (ReCartesian k α β
CartesianId) = forall (k :: * -> * -> *) α. Object k α => IdPattern k α α
IsId
  match_id ReCartesian k α β
_ = forall (k :: * -> * -> *) α β. IdPattern k α β
NotId
  match_compose :: forall α β. ReCartesian k α β -> CompoPattern (ReCartesian k) α β
match_compose (CartesianCompo ReCartesian k α β
f ReCartesian k β β
g) = forall (k :: * -> * -> *) α α γ.
Object k α =>
k α α -> k α γ -> CompoPattern k α γ
IsCompo ReCartesian k α β
f ReCartesian k β β
g
  match_compose 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 :: forall α β. ReCartesian k α β -> SwapPattern (ReCartesian k) α β
match_swap (ReCartesian k α β
CartesianSwap) = forall (k :: * -> * -> *) α γ.
(ObjectPair k α γ, ObjectPair k γ α) =>
SwapPattern k (α, γ) (γ, α)
IsSwap
  match_swap ReCartesian k α β
_ = forall (k :: * -> * -> *) α β. SwapPattern k α β
NotSwap
  match_attachUnit :: forall α β.
ReCartesian k α β -> AttachUnitPattern (ReCartesian k) α β
match_attachUnit (ReCartesian k α β
CartesianAttachUnit) = forall (k :: * -> * -> *) α α.
(Object k α, UnitObject k ~ α, ObjectPair k α α) =>
AttachUnitPattern k α (α, α)
IsAttachUnit
  match_attachUnit ReCartesian k α β
_ = forall (k :: * -> * -> *) α β. AttachUnitPattern k α β
NotAttachUnit
  match_detachUnit :: forall α β.
ReCartesian k α β -> DetachUnitPattern (ReCartesian k) α β
match_detachUnit (ReCartesian k α β
CartesianDetachUnit) = forall (k :: * -> * -> *) α α.
(Object k α, UnitObject k ~ α, ObjectPair k α α) =>
DetachUnitPattern k (α, α) α
IsDetachUnit
  match_detachUnit ReCartesian k α β
_ = forall (k :: * -> * -> *) α β. DetachUnitPattern k α β
NotDetachUnit
  match_regroup :: forall α β. ReCartesian k α β -> RegroupPattern (ReCartesian k) α β
match_regroup (ReCartesian k α β
CartesianRegroup) = forall (k :: * -> * -> *) α γ β.
(ObjectPair k α γ, ObjectPair k γ β, ObjectPair k α (γ, β),
 ObjectPair k (α, γ) β) =>
RegroupPattern k (α, (γ, β)) ((α, γ), β)
IsRegroup
  match_regroup ReCartesian k α β
_ = forall (k :: * -> * -> *) α β. RegroupPattern k α β
NotRegroup
  match_regroup' :: forall α β.
ReCartesian k α β -> Regroup'Pattern (ReCartesian k) α β
match_regroup' (ReCartesian k α β
CartesianRegroup_) = forall (k :: * -> * -> *) α γ β.
(ObjectPair k α γ, ObjectPair k γ β, ObjectPair k α (γ, β),
 ObjectPair k (α, γ) β) =>
Regroup'Pattern k ((α, γ), β) (α, (γ, β))
IsRegroup'
  match_regroup' 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)
-> ((# #) -> r)
-> r
Swap <- (match_swap -> IsSwap)
pattern $mAttachUnit :: forall {r} {k :: * -> * -> *} {α} {β}.
CRCartesian k =>
k α β
-> (forall {u}.
    (β ~ (α, u), UnitObject k ~ u, ObjectPair k α u) =>
    r)
-> ((# #) -> r)
-> r
AttachUnit <- (match_attachUnit -> IsAttachUnit)
pattern $mDetachUnit :: forall {r} {k :: * -> * -> *} {α} {β}.
CRCartesian k =>
k α β
-> (forall {u}.
    (α ~ (β, u), UnitObject k ~ u, ObjectPair k β u) =>
    r)
-> ((# #) -> 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)
-> ((# #) -> 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)
-> ((# #) -> 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 :: forall α β. SpecificCat (ReMorphism k) α β -> ReMorphism k α β
fromSpecific = forall (k :: * -> * -> *) α β. k α β -> ReMorphism k α β
ReMorphism
  match_concrete :: forall α β.
ReMorphism k α β -> Maybe (SpecificCat (ReMorphism k) α β)
match_concrete (ReMorphism k α β
f) = forall a. a -> Maybe a
Just k α β
f
  match_concrete ReMorphism k α β
_ = forall a. Maybe a
Nothing
  match_id :: forall α β. ReMorphism k α β -> IdPattern (ReMorphism k) α β
match_id (ReMorphism k α β
MorphismId) = forall (k :: * -> * -> *) α. Object k α => IdPattern k α α
IsId
  match_id ReMorphism k α β
_ = forall (k :: * -> * -> *) α β. IdPattern k α β
NotId
  match_compose :: forall α β. ReMorphism k α β -> CompoPattern (ReMorphism k) α β
match_compose (MorphismCompo ReMorphism k α β
f ReMorphism k β β
g) = forall (k :: * -> * -> *) α α γ.
Object k α =>
k α α -> k α γ -> CompoPattern k α γ
IsCompo ReMorphism k α β
f ReMorphism k β β
g
  match_compose ReMorphism k α β
_ = forall (k :: * -> * -> *) α β. CompoPattern k α β
NotCompo

instance Morphism k => CRCartesian (ReMorphism k) where
  match_swap :: forall α β. ReMorphism k α β -> SwapPattern (ReMorphism k) α β
match_swap (ReMorphism k α β
MorphismSwap) = forall (k :: * -> * -> *) α γ.
(ObjectPair k α γ, ObjectPair k γ α) =>
SwapPattern k (α, γ) (γ, α)
IsSwap
  match_swap ReMorphism k α β
_ = forall (k :: * -> * -> *) α β. SwapPattern k α β
NotSwap
  match_attachUnit :: forall α β.
ReMorphism k α β -> AttachUnitPattern (ReMorphism k) α β
match_attachUnit (ReMorphism k α β
MorphismAttachUnit) = forall (k :: * -> * -> *) α α.
(Object k α, UnitObject k ~ α, ObjectPair k α α) =>
AttachUnitPattern k α (α, α)
IsAttachUnit
  match_attachUnit ReMorphism k α β
_ = forall (k :: * -> * -> *) α β. AttachUnitPattern k α β
NotAttachUnit
  match_detachUnit :: forall α β.
ReMorphism k α β -> DetachUnitPattern (ReMorphism k) α β
match_detachUnit (ReMorphism k α β
MorphismDetachUnit) = forall (k :: * -> * -> *) α α.
(Object k α, UnitObject k ~ α, ObjectPair k α α) =>
DetachUnitPattern k (α, α) α
IsDetachUnit
  match_detachUnit ReMorphism k α β
_ = forall (k :: * -> * -> *) α β. DetachUnitPattern k α β
NotDetachUnit
  match_regroup :: forall α β. ReMorphism k α β -> RegroupPattern (ReMorphism k) α β
match_regroup (ReMorphism k α β
MorphismRegroup) = forall (k :: * -> * -> *) α γ β.
(ObjectPair k α γ, ObjectPair k γ β, ObjectPair k α (γ, β),
 ObjectPair k (α, γ) β) =>
RegroupPattern k (α, (γ, β)) ((α, γ), β)
IsRegroup
  match_regroup ReMorphism k α β
_ = forall (k :: * -> * -> *) α β. RegroupPattern k α β
NotRegroup
  match_regroup' :: forall α β. ReMorphism k α β -> Regroup'Pattern (ReMorphism k) α β
match_regroup' (ReMorphism k α β
MorphismRegroup_) = forall (k :: * -> * -> *) α γ β.
(ObjectPair k α γ, ObjectPair k γ β, ObjectPair k α (γ, β),
 ObjectPair k (α, γ) β) =>
Regroup'Pattern k ((α, γ), β) (α, (γ, β))
IsRegroup'
  match_regroup' 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 :: forall α β. ReMorphism k α β -> ParPattern (ReMorphism k) α β
match_par (MorphismPar ReMorphism k α β
f ReMorphism k γ δ
g) = forall (k :: * -> * -> *) α γ β δ.
(ObjectPair k α γ, ObjectPair k β δ) =>
k α β -> k γ δ -> ParPattern k (α, γ) (β, δ)
IsPar ReMorphism k α β
f ReMorphism k γ δ
g
  match_par 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)
-> ((# #) -> 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 :: forall α β. SpecificCat (RePreArrow k) α β -> RePreArrow k α β
fromSpecific = forall (k :: * -> * -> *) α β. k α β -> RePreArrow k α β
RePreArrow
  match_concrete :: forall α β.
RePreArrow k α β -> Maybe (SpecificCat (RePreArrow k) α β)
match_concrete (RePreArrow k α β
f) = forall a. a -> Maybe a
Just k α β
f
  match_concrete RePreArrow k α β
_ = forall a. Maybe a
Nothing
  match_id :: forall α β. RePreArrow k α β -> IdPattern (RePreArrow k) α β
match_id (RePreArrow k α β
PreArrowId) = forall (k :: * -> * -> *) α. Object k α => IdPattern k α α
IsId
  match_id RePreArrow k α β
_ = forall (k :: * -> * -> *) α β. IdPattern k α β
NotId
  match_compose :: forall α β. RePreArrow k α β -> CompoPattern (RePreArrow k) α β
match_compose (PreArrowCompo RePreArrow k α β
f RePreArrow k β β
g) = forall (k :: * -> * -> *) α α γ.
Object k α =>
k α α -> k α γ -> CompoPattern k α γ
IsCompo RePreArrow k α β
f RePreArrow k β β
g
  match_compose RePreArrow k α β
_ = forall (k :: * -> * -> *) α β. CompoPattern k α β
NotCompo

instance PreArrow k => CRCartesian (RePreArrow k) where
  match_swap :: forall α β. RePreArrow k α β -> SwapPattern (RePreArrow k) α β
match_swap (RePreArrow k α β
PreArrowSwap) = forall (k :: * -> * -> *) α γ.
(ObjectPair k α γ, ObjectPair k γ α) =>
SwapPattern k (α, γ) (γ, α)
IsSwap
  match_swap RePreArrow k α β
_ = forall (k :: * -> * -> *) α β. SwapPattern k α β
NotSwap
  match_attachUnit :: forall α β.
RePreArrow k α β -> AttachUnitPattern (RePreArrow k) α β
match_attachUnit (RePreArrow k α β
PreArrowAttachUnit) = forall (k :: * -> * -> *) α α.
(Object k α, UnitObject k ~ α, ObjectPair k α α) =>
AttachUnitPattern k α (α, α)
IsAttachUnit
  match_attachUnit RePreArrow k α β
_ = forall (k :: * -> * -> *) α β. AttachUnitPattern k α β
NotAttachUnit
  match_detachUnit :: forall α β.
RePreArrow k α β -> DetachUnitPattern (RePreArrow k) α β
match_detachUnit (RePreArrow k α β
PreArrowDetachUnit) = forall (k :: * -> * -> *) α α.
(Object k α, UnitObject k ~ α, ObjectPair k α α) =>
DetachUnitPattern k (α, α) α
IsDetachUnit
  match_detachUnit RePreArrow k α β
_ = forall (k :: * -> * -> *) α β. DetachUnitPattern k α β
NotDetachUnit
  match_regroup :: forall α β. RePreArrow k α β -> RegroupPattern (RePreArrow k) α β
match_regroup (RePreArrow k α β
PreArrowRegroup) = forall (k :: * -> * -> *) α γ β.
(ObjectPair k α γ, ObjectPair k γ β, ObjectPair k α (γ, β),
 ObjectPair k (α, γ) β) =>
RegroupPattern k (α, (γ, β)) ((α, γ), β)
IsRegroup
  match_regroup RePreArrow k α β
_ = forall (k :: * -> * -> *) α β. RegroupPattern k α β
NotRegroup
  match_regroup' :: forall α β. RePreArrow k α β -> Regroup'Pattern (RePreArrow k) α β
match_regroup' (RePreArrow k α β
PreArrowRegroup_) = forall (k :: * -> * -> *) α γ β.
(ObjectPair k α γ, ObjectPair k γ β, ObjectPair k α (γ, β),
 ObjectPair k (α, γ) β) =>
Regroup'Pattern k ((α, γ), β) (α, (γ, β))
IsRegroup'
  match_regroup' RePreArrow k α β
_ = forall (k :: * -> * -> *) α β. Regroup'Pattern k α β
NotRegroup'

instance PreArrow k => CRMorphism (RePreArrow k) where
  match_par :: forall α β. RePreArrow k α β -> ParPattern (RePreArrow k) α β
match_par (PreArrowPar RePreArrow k α β
f RePreArrow k γ δ
g) = forall (k :: * -> * -> *) α γ β δ.
(ObjectPair k α γ, ObjectPair k β δ) =>
k α β -> k γ δ -> ParPattern k (α, γ) (β, δ)
IsPar RePreArrow k α β
f RePreArrow k γ δ
g
  match_par 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)
-> ((# #) -> r)
-> r
:&&&g <- (match_fan -> IsFan f g)
pattern $mFst :: forall {r} {k :: * -> * -> *} {α} {β}.
CRPreArrow k =>
k α β
-> (forall {β1}. (α ~ (β, β1), ObjectPair k β β1) => r)
-> ((# #) -> r)
-> r
Fst <- (match_fst -> IsFst)
pattern $mSnd :: forall {r} {k :: * -> * -> *} {α} {β}.
CRPreArrow k =>
k α β
-> (forall {α1}. (α ~ (α1, β), ObjectPair k α1 β) => r)
-> ((# #) -> r)
-> r
Snd <- (match_snd -> IsSnd)
pattern $mTerminal :: forall {r} {k :: * -> * -> *} {α} {β}.
CRPreArrow k =>
k α β -> ((Object k α, UnitObject k ~ β) => r) -> ((# #) -> r) -> r
Terminal <- (match_terminal -> IsTerminal)
#endif
  
instance PreArrow k => CRPreArrow (RePreArrow k) where
  match_fan :: forall α β. RePreArrow k α β -> FanPattern (RePreArrow k) α β
match_fan (PreArrowFanout RePreArrow k α β
f RePreArrow k α γ
g) = forall (k :: * -> * -> *) α α γ.
(Object k α, ObjectPair k α γ) =>
k α α -> k α γ -> FanPattern k α (α, γ)
IsFan RePreArrow k α β
f RePreArrow k α γ
g
  match_fan RePreArrow k α β
_ = forall (k :: * -> * -> *) α β. FanPattern k α β
NotFan
  match_fst :: forall α β. RePreArrow k α β -> FstPattern (RePreArrow k) α β
match_fst RePreArrow k α β
PreArrowFst = forall (k :: * -> * -> *) α α.
ObjectPair k α α =>
FstPattern k (α, α) α
IsFst
  match_fst RePreArrow k α β
_ = forall (k :: * -> * -> *) α β. FstPattern k α β
NotFst
  match_snd :: forall α β. RePreArrow k α β -> SndPattern (RePreArrow k) α β
match_snd RePreArrow k α β
PreArrowSnd = forall (k :: * -> * -> *) α β.
ObjectPair k α β =>
SndPattern k (α, β) β
IsSnd
  match_snd RePreArrow k α β
_ = forall (k :: * -> * -> *) α β. SndPattern k α β
NotSnd
  match_terminal :: forall α β. RePreArrow k α β -> TerminalPattern (RePreArrow k) α β
match_terminal RePreArrow k α β
PreArrowTerminal = forall (k :: * -> * -> *) α u.
(Object k α, UnitObject k ~ u) =>
TerminalPattern k α u
IsTerminal
  match_terminal RePreArrow k α β
_ = forall (k :: * -> * -> *) α β. TerminalPattern k α β
NotTerminal


instance WellPointed k => CRCategory (ReWellPointed k) where
  type SpecificCat (ReWellPointed k) = k
  fromSpecific :: forall α β.
SpecificCat (ReWellPointed k) α β -> ReWellPointed k α β
fromSpecific = forall (k :: * -> * -> *) α β. k α β -> ReWellPointed k α β
ReWellPointed
  match_concrete :: forall α β.
ReWellPointed k α β -> Maybe (SpecificCat (ReWellPointed k) α β)
match_concrete (ReWellPointed k α β
f) = forall a. a -> Maybe a
Just k α β
f
  match_concrete ReWellPointed k α β
_ = forall a. Maybe a
Nothing
  match_id :: forall α β. ReWellPointed k α β -> IdPattern (ReWellPointed k) α β
match_id (ReWellPointed k α β
WellPointedId) = forall (k :: * -> * -> *) α. Object k α => IdPattern k α α
IsId
  match_id ReWellPointed k α β
_ = forall (k :: * -> * -> *) α β. IdPattern k α β
NotId
  match_compose :: forall α β.
ReWellPointed k α β -> CompoPattern (ReWellPointed k) α β
match_compose (WellPointedCompo ReWellPointed k α β
f ReWellPointed k β β
g) = forall (k :: * -> * -> *) α α γ.
Object k α =>
k α α -> k α γ -> CompoPattern k α γ
IsCompo ReWellPointed k α β
f ReWellPointed k β β
g
  match_compose ReWellPointed k α β
_ = forall (k :: * -> * -> *) α β. CompoPattern k α β
NotCompo

instance WellPointed k => CRCartesian (ReWellPointed k) where
  match_swap :: forall α β.
ReWellPointed k α β -> SwapPattern (ReWellPointed k) α β
match_swap (ReWellPointed k α β
WellPointedSwap) = forall (k :: * -> * -> *) α γ.
(ObjectPair k α γ, ObjectPair k γ α) =>
SwapPattern k (α, γ) (γ, α)
IsSwap
  match_swap ReWellPointed k α β
_ = forall (k :: * -> * -> *) α β. SwapPattern k α β
NotSwap
  match_attachUnit :: forall α β.
ReWellPointed k α β -> AttachUnitPattern (ReWellPointed k) α β
match_attachUnit (ReWellPointed k α β
WellPointedAttachUnit) = forall (k :: * -> * -> *) α α.
(Object k α, UnitObject k ~ α, ObjectPair k α α) =>
AttachUnitPattern k α (α, α)
IsAttachUnit
  match_attachUnit ReWellPointed k α β
_ = forall (k :: * -> * -> *) α β. AttachUnitPattern k α β
NotAttachUnit
  match_detachUnit :: forall α β.
ReWellPointed k α β -> DetachUnitPattern (ReWellPointed k) α β
match_detachUnit (ReWellPointed k α β
WellPointedDetachUnit) = forall (k :: * -> * -> *) α α.
(Object k α, UnitObject k ~ α, ObjectPair k α α) =>
DetachUnitPattern k (α, α) α
IsDetachUnit
  match_detachUnit ReWellPointed k α β
_ = forall (k :: * -> * -> *) α β. DetachUnitPattern k α β
NotDetachUnit
  match_regroup :: forall α β.
ReWellPointed k α β -> RegroupPattern (ReWellPointed k) α β
match_regroup (ReWellPointed k α β
WellPointedRegroup) = forall (k :: * -> * -> *) α γ β.
(ObjectPair k α γ, ObjectPair k γ β, ObjectPair k α (γ, β),
 ObjectPair k (α, γ) β) =>
RegroupPattern k (α, (γ, β)) ((α, γ), β)
IsRegroup
  match_regroup ReWellPointed k α β
_ = forall (k :: * -> * -> *) α β. RegroupPattern k α β
NotRegroup
  match_regroup' :: forall α β.
ReWellPointed k α β -> Regroup'Pattern (ReWellPointed k) α β
match_regroup' (ReWellPointed k α β
WellPointedRegroup_) = forall (k :: * -> * -> *) α γ β.
(ObjectPair k α γ, ObjectPair k γ β, ObjectPair k α (γ, β),
 ObjectPair k (α, γ) β) =>
Regroup'Pattern k ((α, γ), β) (α, (γ, β))
IsRegroup'
  match_regroup' ReWellPointed k α β
_ = forall (k :: * -> * -> *) α β. Regroup'Pattern k α β
NotRegroup'

instance WellPointed k => CRMorphism (ReWellPointed k) where
  match_par :: forall α β. ReWellPointed k α β -> ParPattern (ReWellPointed k) α β
match_par (WellPointedPar ReWellPointed k α β
f ReWellPointed k γ δ
g) = forall (k :: * -> * -> *) α γ β δ.
(ObjectPair k α γ, ObjectPair k β δ) =>
k α β -> k γ δ -> ParPattern k (α, γ) (β, δ)
IsPar ReWellPointed k α β
f ReWellPointed k γ δ
g
  match_par ReWellPointed k α β
_ = forall (k :: * -> * -> *) α β. ParPattern k α β
NotPar
  
instance WellPointed k => CRPreArrow (ReWellPointed k) where
  match_fan :: forall α β. ReWellPointed k α β -> FanPattern (ReWellPointed k) α β
match_fan (WellPointedFanout ReWellPointed k α β
f ReWellPointed k α γ
g) = forall (k :: * -> * -> *) α α γ.
(Object k α, ObjectPair k α γ) =>
k α α -> k α γ -> FanPattern k α (α, γ)
IsFan ReWellPointed k α β
f ReWellPointed k α γ
g
  match_fan ReWellPointed k α β
_ = forall (k :: * -> * -> *) α β. FanPattern k α β
NotFan
  match_fst :: forall α β. ReWellPointed k α β -> FstPattern (ReWellPointed k) α β
match_fst ReWellPointed k α β
WellPointedFst = forall (k :: * -> * -> *) α α.
ObjectPair k α α =>
FstPattern k (α, α) α
IsFst
  match_fst ReWellPointed k α β
_ = forall (k :: * -> * -> *) α β. FstPattern k α β
NotFst
  match_snd :: forall α β. ReWellPointed k α β -> SndPattern (ReWellPointed k) α β
match_snd ReWellPointed k α β
WellPointedSnd = forall (k :: * -> * -> *) α β.
ObjectPair k α β =>
SndPattern k (α, β) β
IsSnd
  match_snd ReWellPointed k α β
_ = forall (k :: * -> * -> *) α β. SndPattern k α β
NotSnd
  match_terminal :: forall α β.
ReWellPointed k α β -> TerminalPattern (ReWellPointed k) α β
match_terminal ReWellPointed k α β
WellPointedTerminal = forall (k :: * -> * -> *) α u.
(Object k α, UnitObject k ~ u) =>
TerminalPattern k α u
IsTerminal
  match_terminal 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) -> ((# #) -> r) -> r
Const c <- (match_const -> IsConst c)
#endif
  
instance WellPointed k => CRWellPointed (ReWellPointed k) where
  match_const :: forall α β.
ReWellPointed k α β -> ConstPattern (ReWellPointed k) α β
match_const (WellPointedConst β
c) = forall (k :: * -> * -> *) α β.
(Object k α, Object k β) =>
β -> ConstPattern k α β
IsConst β
c
  match_const ReWellPointed k α β
_ = forall (k :: * -> * -> *) α β. ConstPattern k α β
NotConst