-- |
-- 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 :: 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