{-# LANGUAGE PostfixOperators #-}
{-# OPTIONS_HADDOCK prune #-}
----------------------------------------------------------------------------
-- |
-- Module      :  ForSyDe.Atom.ExB
-- Copyright   :  (c) George Ungureanu, 2015-2017
-- License     :  BSD-style (see the file LICENSE)
-- 
-- Maintainer  :  ugeorge@kth.se
-- Stability   :  experimental
-- Portability :  portable
--
-- This module exports the core entities of the extended behavior
-- layer: interfaces for atoms and common patterns of atoms. It does
-- /NOT/ export any implementation or instantiation of any specific
-- behavior extension type.  For an overview about atoms, layers and
-- patterns, please refer to the "ForSyDe.Atom" module documentation.
--
-- __IMPORTANT!!!__
-- see the <ForSyDe-Atom.html#naming_conv naming convention> rules
-- on how to interpret, use and develop your own constructors.
----------------------------------------------------------------------------
module ForSyDe.Atom.ExB (

  -- * Atoms

  ExB (..),
  
  -- * Patterns

  res11, res12, res13, res14,
  res21, res22, res23, res24,
  res31, res32, res33, res34,
  res41, res42, res43, res44,
  res51, res52, res53, res54,
  res61, res62, res63, res64,
  res71, res72, res73, res74,
  res81, res82, res83, res84,

  filter, filter',

  degen,

  ignore11, ignore12, ignore13, ignore14,
  ignore21, ignore22, ignore23, ignore24,
  ignore31, ignore32, ignore33, ignore34,
  ignore41, ignore42, ignore43, ignore44
  
  ) where

import Prelude hiding (filter)
import ForSyDe.Atom.Utility.Tuple

infixl 4 /.\, /*\, /&\, /!\

-- | Class which defines the atoms for the extended behavior layer.
--
-- As its name suggests, this layer is extending the behavior of the
-- wrapped entity/function by expanding its domains set with symbols
-- having clearly defined semantics (e.g. special events with known
-- responses).
--
-- The types associated with this layer can simply be describes as:
--
-- <<fig/eqs-exb-types.png>>
--
-- where \(\alpha\) is a base type and \(b\) is the type extension,
-- i.e. a set of symbols with clearly defined semantics.
--
-- Extended behavior atoms are functions of these types, defined as
-- interfaces in the 'ExB' type class.
class Functor b => ExB b where
  -- | Extends a value (from a layer below) with a set of symbols with
  -- known semantics, as described by a type instantiating this class.
  extend :: a -> b a

  -- | Basic functor operator. Lifts a function (from a layer below)
  -- into the domain of the extended behavior layer.
  --
  -- <<fig/eqs-exb-atom-func.png>>
  (/.\) :: (a -> a') -> b a -> b a'

  -- | Applicative operator. Defines a resolution between two extended
  -- behavior symbols.
  --
  -- <<fig/eqs-exb-atom-app.png>>
  (/*\) :: b (a -> a') -> b a -> b a'

  -- | Predicate operator. Generates a defined behavior based on an
  -- extended Boolean predicate.
  --
  -- <<fig/eqs-exb-atom-phi.png>>
  (/&\) :: b Bool -> b a -> b a

  -- | Degenerate operator. Degenerates a behavior-extended value into
  -- a non-extended one (from a layer below), based on a kernel
  -- value. Used also to throw exceptions.
  --
  -- <<fig/eqs-exb-atom-deg.png>>
  (/!\) :: a -> b a -> a

-- |  
-- <<fig/eqs-exb-pattern-resolution.png>>
--
-- The @res@ behavior pattern lifts a function on values to the
-- extended behavior domain, and applies a resolution between two
-- extended behavior symbols.
--
-- Constructors: @res[1-8][1-4]@.
res22 :: ExB b
  => (a1 -> a2 -> (a1', a2')) -- ^ function on values
  -> b a1                     -- ^ first input
  -> b a2                     -- ^ second input
  -> (b a1', b a2')           -- ^ tupled output
  
res11 :: (a -> a') -> b a -> b a'
res11 f :: a -> a'
f b1 :: b a
b1                      = (a -> a'
f (a -> a') -> b a -> b a'
forall (b :: * -> *) a a'. ExB b => (a -> a') -> b a -> b a'
/.\ b a
b1)
res21 :: (a -> a -> a') -> b a -> b a -> b a'
res21 f :: a -> a -> a'
f b1 :: b a
b1 b2 :: b a
b2                   = (a -> a -> a'
f (a -> a -> a') -> b a -> b (a -> a')
forall (b :: * -> *) a a'. ExB b => (a -> a') -> b a -> b a'
/.\ b a
b1 b (a -> a') -> b a -> b a'
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ b a
b2)
res31 :: (a -> a -> a -> a') -> b a -> b a -> b a -> b a'
res31 f :: a -> a -> a -> a'
f b1 :: b a
b1 b2 :: b a
b2 b3 :: b a
b3                = (a -> a -> a -> a'
f (a -> a -> a -> a') -> b a -> b (a -> a -> a')
forall (b :: * -> *) a a'. ExB b => (a -> a') -> b a -> b a'
/.\ b a
b1 b (a -> a -> a') -> b a -> b (a -> a')
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ b a
b2 b (a -> a') -> b a -> b a'
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ b a
b3)
res41 :: (a -> a -> a -> a -> a') -> b a -> b a -> b a -> b a -> b a'
res41 f :: a -> a -> a -> a -> a'
f b1 :: b a
b1 b2 :: b a
b2 b3 :: b a
b3 b4 :: b a
b4             = (a -> a -> a -> a -> a'
f (a -> a -> a -> a -> a') -> b a -> b (a -> a -> a -> a')
forall (b :: * -> *) a a'. ExB b => (a -> a') -> b a -> b a'
/.\ b a
b1 b (a -> a -> a -> a') -> b a -> b (a -> a -> a')
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ b a
b2 b (a -> a -> a') -> b a -> b (a -> a')
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ b a
b3 b (a -> a') -> b a -> b a'
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ b a
b4)
res51 :: (a -> a -> a -> a -> a -> a')
-> b a -> b a -> b a -> b a -> b a -> b a'
res51 f :: a -> a -> a -> a -> a -> a'
f b1 :: b a
b1 b2 :: b a
b2 b3 :: b a
b3 b4 :: b a
b4 b5 :: b a
b5          = (a -> a -> a -> a -> a -> a'
f (a -> a -> a -> a -> a -> a') -> b a -> b (a -> a -> a -> a -> a')
forall (b :: * -> *) a a'. ExB b => (a -> a') -> b a -> b a'
/.\ b a
b1 b (a -> a -> a -> a -> a') -> b a -> b (a -> a -> a -> a')
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ b a
b2 b (a -> a -> a -> a') -> b a -> b (a -> a -> a')
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ b a
b3 b (a -> a -> a') -> b a -> b (a -> a')
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ b a
b4 b (a -> a') -> b a -> b a'
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ b a
b5)
res61 :: (a -> a -> a -> a -> a -> a -> a')
-> b a -> b a -> b a -> b a -> b a -> b a -> b a'
res61 f :: a -> a -> a -> a -> a -> a -> a'
f b1 :: b a
b1 b2 :: b a
b2 b3 :: b a
b3 b4 :: b a
b4 b5 :: b a
b5 b6 :: b a
b6       = (a -> a -> a -> a -> a -> a -> a'
f (a -> a -> a -> a -> a -> a -> a')
-> b a -> b (a -> a -> a -> a -> a -> a')
forall (b :: * -> *) a a'. ExB b => (a -> a') -> b a -> b a'
/.\ b a
b1 b (a -> a -> a -> a -> a -> a')
-> b a -> b (a -> a -> a -> a -> a')
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ b a
b2 b (a -> a -> a -> a -> a') -> b a -> b (a -> a -> a -> a')
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ b a
b3 b (a -> a -> a -> a') -> b a -> b (a -> a -> a')
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ b a
b4 b (a -> a -> a') -> b a -> b (a -> a')
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ b a
b5 b (a -> a') -> b a -> b a'
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ b a
b6)
res71 :: (a -> a -> a -> a -> a -> a -> a -> a')
-> b a -> b a -> b a -> b a -> b a -> b a -> b a -> b a'
res71 f :: a -> a -> a -> a -> a -> a -> a -> a'
f b1 :: b a
b1 b2 :: b a
b2 b3 :: b a
b3 b4 :: b a
b4 b5 :: b a
b5 b6 :: b a
b6 b7 :: b a
b7    = (a -> a -> a -> a -> a -> a -> a -> a'
f (a -> a -> a -> a -> a -> a -> a -> a')
-> b a -> b (a -> a -> a -> a -> a -> a -> a')
forall (b :: * -> *) a a'. ExB b => (a -> a') -> b a -> b a'
/.\ b a
b1 b (a -> a -> a -> a -> a -> a -> a')
-> b a -> b (a -> a -> a -> a -> a -> a')
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ b a
b2 b (a -> a -> a -> a -> a -> a')
-> b a -> b (a -> a -> a -> a -> a')
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ b a
b3 b (a -> a -> a -> a -> a') -> b a -> b (a -> a -> a -> a')
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ b a
b4 b (a -> a -> a -> a') -> b a -> b (a -> a -> a')
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ b a
b5 b (a -> a -> a') -> b a -> b (a -> a')
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ b a
b6 b (a -> a') -> b a -> b a'
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ b a
b7)
res81 :: (a -> a -> a -> a -> a -> a -> a -> a -> a')
-> b a -> b a -> b a -> b a -> b a -> b a -> b a -> b a -> b a'
res81 f :: a -> a -> a -> a -> a -> a -> a -> a -> a'
f b1 :: b a
b1 b2 :: b a
b2 b3 :: b a
b3 b4 :: b a
b4 b5 :: b a
b5 b6 :: b a
b6 b7 :: b a
b7 b8 :: b a
b8 = (a -> a -> a -> a -> a -> a -> a -> a -> a'
f (a -> a -> a -> a -> a -> a -> a -> a -> a')
-> b a -> b (a -> a -> a -> a -> a -> a -> a -> a')
forall (b :: * -> *) a a'. ExB b => (a -> a') -> b a -> b a'
/.\ b a
b1 b (a -> a -> a -> a -> a -> a -> a -> a')
-> b a -> b (a -> a -> a -> a -> a -> a -> a')
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ b a
b2 b (a -> a -> a -> a -> a -> a -> a')
-> b a -> b (a -> a -> a -> a -> a -> a')
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ b a
b3 b (a -> a -> a -> a -> a -> a')
-> b a -> b (a -> a -> a -> a -> a')
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ b a
b4 b (a -> a -> a -> a -> a') -> b a -> b (a -> a -> a -> a')
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ b a
b5 b (a -> a -> a -> a') -> b a -> b (a -> a -> a')
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ b a
b6 b (a -> a -> a') -> b a -> b (a -> a')
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ b a
b7 b (a -> a') -> b a -> b a'
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ b a
b8)
res12 :: (a -> (a1, b)) -> f a -> (f a1, f b)
res12 f :: a -> (a1, b)
f b1 :: f a
b1                      = (a -> (a1, b)
f (a -> (a1, b)) -> f a -> f (a1, b)
forall (b :: * -> *) a a'. ExB b => (a -> a') -> b a -> b a'
/.\ f a
b1 f (a1, b) -> (f a1, f b)
forall (f :: * -> *) a1 b. Functor f => f (a1, b) -> (f a1, f b)
|<)
res22 :: (a1 -> a2 -> (a1', a2')) -> b a1 -> b a2 -> (b a1', b a2')
res22 f :: a1 -> a2 -> (a1', a2')
f b1 :: b a1
b1 b2 :: b a2
b2                   = (a1 -> a2 -> (a1', a2')
f (a1 -> a2 -> (a1', a2')) -> b a1 -> b (a2 -> (a1', a2'))
forall (b :: * -> *) a a'. ExB b => (a -> a') -> b a -> b a'
/.\ b a1
b1 b (a2 -> (a1', a2')) -> b a2 -> b (a1', a2')
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ b a2
b2 b (a1', a2') -> (b a1', b a2')
forall (f :: * -> *) a1 b. Functor f => f (a1, b) -> (f a1, f b)
|<)
res32 :: (a -> a -> a -> (a1, b)) -> f a -> f a -> f a -> (f a1, f b)
res32 f :: a -> a -> a -> (a1, b)
f b1 :: f a
b1 b2 :: f a
b2 b3 :: f a
b3                = (a -> a -> a -> (a1, b)
f (a -> a -> a -> (a1, b)) -> f a -> f (a -> a -> (a1, b))
forall (b :: * -> *) a a'. ExB b => (a -> a') -> b a -> b a'
/.\ f a
b1 f (a -> a -> (a1, b)) -> f a -> f (a -> (a1, b))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b2 f (a -> (a1, b)) -> f a -> f (a1, b)
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b3 f (a1, b) -> (f a1, f b)
forall (f :: * -> *) a1 b. Functor f => f (a1, b) -> (f a1, f b)
|<)
res42 :: (a -> a -> a -> a -> (a1, b))
-> f a -> f a -> f a -> f a -> (f a1, f b)
res42 f :: a -> a -> a -> a -> (a1, b)
f b1 :: f a
b1 b2 :: f a
b2 b3 :: f a
b3 b4 :: f a
b4             = (a -> a -> a -> a -> (a1, b)
f (a -> a -> a -> a -> (a1, b)) -> f a -> f (a -> a -> a -> (a1, b))
forall (b :: * -> *) a a'. ExB b => (a -> a') -> b a -> b a'
/.\ f a
b1 f (a -> a -> a -> (a1, b)) -> f a -> f (a -> a -> (a1, b))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b2 f (a -> a -> (a1, b)) -> f a -> f (a -> (a1, b))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b3 f (a -> (a1, b)) -> f a -> f (a1, b)
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b4 f (a1, b) -> (f a1, f b)
forall (f :: * -> *) a1 b. Functor f => f (a1, b) -> (f a1, f b)
|<)
res52 :: (a -> a -> a -> a -> a -> (a1, b))
-> f a -> f a -> f a -> f a -> f a -> (f a1, f b)
res52 f :: a -> a -> a -> a -> a -> (a1, b)
f b1 :: f a
b1 b2 :: f a
b2 b3 :: f a
b3 b4 :: f a
b4 b5 :: f a
b5          = (a -> a -> a -> a -> a -> (a1, b)
f (a -> a -> a -> a -> a -> (a1, b))
-> f a -> f (a -> a -> a -> a -> (a1, b))
forall (b :: * -> *) a a'. ExB b => (a -> a') -> b a -> b a'
/.\ f a
b1 f (a -> a -> a -> a -> (a1, b))
-> f a -> f (a -> a -> a -> (a1, b))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b2 f (a -> a -> a -> (a1, b)) -> f a -> f (a -> a -> (a1, b))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b3 f (a -> a -> (a1, b)) -> f a -> f (a -> (a1, b))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b4 f (a -> (a1, b)) -> f a -> f (a1, b)
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b5 f (a1, b) -> (f a1, f b)
forall (f :: * -> *) a1 b. Functor f => f (a1, b) -> (f a1, f b)
|<)
res62 :: (a -> a -> a -> a -> a -> a -> (a1, b))
-> f a -> f a -> f a -> f a -> f a -> f a -> (f a1, f b)
res62 f :: a -> a -> a -> a -> a -> a -> (a1, b)
f b1 :: f a
b1 b2 :: f a
b2 b3 :: f a
b3 b4 :: f a
b4 b5 :: f a
b5 b6 :: f a
b6       = (a -> a -> a -> a -> a -> a -> (a1, b)
f (a -> a -> a -> a -> a -> a -> (a1, b))
-> f a -> f (a -> a -> a -> a -> a -> (a1, b))
forall (b :: * -> *) a a'. ExB b => (a -> a') -> b a -> b a'
/.\ f a
b1 f (a -> a -> a -> a -> a -> (a1, b))
-> f a -> f (a -> a -> a -> a -> (a1, b))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b2 f (a -> a -> a -> a -> (a1, b))
-> f a -> f (a -> a -> a -> (a1, b))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b3 f (a -> a -> a -> (a1, b)) -> f a -> f (a -> a -> (a1, b))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b4 f (a -> a -> (a1, b)) -> f a -> f (a -> (a1, b))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b5 f (a -> (a1, b)) -> f a -> f (a1, b)
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b6 f (a1, b) -> (f a1, f b)
forall (f :: * -> *) a1 b. Functor f => f (a1, b) -> (f a1, f b)
|<)
res72 :: (a -> a -> a -> a -> a -> a -> a -> (a1, b))
-> f a -> f a -> f a -> f a -> f a -> f a -> f a -> (f a1, f b)
res72 f :: a -> a -> a -> a -> a -> a -> a -> (a1, b)
f b1 :: f a
b1 b2 :: f a
b2 b3 :: f a
b3 b4 :: f a
b4 b5 :: f a
b5 b6 :: f a
b6 b7 :: f a
b7    = (a -> a -> a -> a -> a -> a -> a -> (a1, b)
f (a -> a -> a -> a -> a -> a -> a -> (a1, b))
-> f a -> f (a -> a -> a -> a -> a -> a -> (a1, b))
forall (b :: * -> *) a a'. ExB b => (a -> a') -> b a -> b a'
/.\ f a
b1 f (a -> a -> a -> a -> a -> a -> (a1, b))
-> f a -> f (a -> a -> a -> a -> a -> (a1, b))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b2 f (a -> a -> a -> a -> a -> (a1, b))
-> f a -> f (a -> a -> a -> a -> (a1, b))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b3 f (a -> a -> a -> a -> (a1, b))
-> f a -> f (a -> a -> a -> (a1, b))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b4 f (a -> a -> a -> (a1, b)) -> f a -> f (a -> a -> (a1, b))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b5 f (a -> a -> (a1, b)) -> f a -> f (a -> (a1, b))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b6 f (a -> (a1, b)) -> f a -> f (a1, b)
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b7 f (a1, b) -> (f a1, f b)
forall (f :: * -> *) a1 b. Functor f => f (a1, b) -> (f a1, f b)
|<)
res82 :: (a -> a -> a -> a -> a -> a -> a -> a -> (a1, b))
-> f a
-> f a
-> f a
-> f a
-> f a
-> f a
-> p
-> f a
-> (f a1, f b)
res82 f :: a -> a -> a -> a -> a -> a -> a -> a -> (a1, b)
f b1 :: f a
b1 b2 :: f a
b2 b3 :: f a
b3 b4 :: f a
b4 b5 :: f a
b5 b6 :: f a
b6 b7 :: p
b7 b8 :: f a
b8 = (a -> a -> a -> a -> a -> a -> a -> a -> (a1, b)
f (a -> a -> a -> a -> a -> a -> a -> a -> (a1, b))
-> f a -> f (a -> a -> a -> a -> a -> a -> a -> (a1, b))
forall (b :: * -> *) a a'. ExB b => (a -> a') -> b a -> b a'
/.\ f a
b1 f (a -> a -> a -> a -> a -> a -> a -> (a1, b))
-> f a -> f (a -> a -> a -> a -> a -> a -> (a1, b))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b2 f (a -> a -> a -> a -> a -> a -> (a1, b))
-> f a -> f (a -> a -> a -> a -> a -> (a1, b))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b3 f (a -> a -> a -> a -> a -> (a1, b))
-> f a -> f (a -> a -> a -> a -> (a1, b))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b4 f (a -> a -> a -> a -> (a1, b))
-> f a -> f (a -> a -> a -> (a1, b))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b5 f (a -> a -> a -> (a1, b)) -> f a -> f (a -> a -> (a1, b))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b6 f (a -> a -> (a1, b)) -> f a -> f (a -> (a1, b))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b5 f (a -> (a1, b)) -> f a -> f (a1, b)
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b8 f (a1, b) -> (f a1, f b)
forall (f :: * -> *) a1 b. Functor f => f (a1, b) -> (f a1, f b)
|<)
res13 :: (a -> (a, b1, b2)) -> f a -> (f a, f b1, f b2)
res13 f :: a -> (a, b1, b2)
f b1 :: f a
b1                      = (a -> (a, b1, b2)
f (a -> (a, b1, b2)) -> f a -> f (a, b1, b2)
forall (b :: * -> *) a a'. ExB b => (a -> a') -> b a -> b a'
/.\ f a
b1 f (a, b1, b2) -> (f a, f b1, f b2)
forall (f :: * -> *) a b1 b2.
Functor f =>
f (a, b1, b2) -> (f a, f b1, f b2)
|<<)
res23 :: (a -> a -> (a, b1, b2)) -> f a -> f a -> (f a, f b1, f b2)
res23 f :: a -> a -> (a, b1, b2)
f b1 :: f a
b1 b2 :: f a
b2                   = (a -> a -> (a, b1, b2)
f (a -> a -> (a, b1, b2)) -> f a -> f (a -> (a, b1, b2))
forall (b :: * -> *) a a'. ExB b => (a -> a') -> b a -> b a'
/.\ f a
b1 f (a -> (a, b1, b2)) -> f a -> f (a, b1, b2)
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b2 f (a, b1, b2) -> (f a, f b1, f b2)
forall (f :: * -> *) a b1 b2.
Functor f =>
f (a, b1, b2) -> (f a, f b1, f b2)
|<<)
res33 :: (a -> a -> a -> (a, b1, b2))
-> f a -> f a -> f a -> (f a, f b1, f b2)
res33 f :: a -> a -> a -> (a, b1, b2)
f b1 :: f a
b1 b2 :: f a
b2 b3 :: f a
b3                = (a -> a -> a -> (a, b1, b2)
f (a -> a -> a -> (a, b1, b2)) -> f a -> f (a -> a -> (a, b1, b2))
forall (b :: * -> *) a a'. ExB b => (a -> a') -> b a -> b a'
/.\ f a
b1 f (a -> a -> (a, b1, b2)) -> f a -> f (a -> (a, b1, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b2 f (a -> (a, b1, b2)) -> f a -> f (a, b1, b2)
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b3 f (a, b1, b2) -> (f a, f b1, f b2)
forall (f :: * -> *) a b1 b2.
Functor f =>
f (a, b1, b2) -> (f a, f b1, f b2)
|<<)
res43 :: (a -> a -> a -> a -> (a, b1, b2))
-> f a -> f a -> f a -> f a -> (f a, f b1, f b2)
res43 f :: a -> a -> a -> a -> (a, b1, b2)
f b1 :: f a
b1 b2 :: f a
b2 b3 :: f a
b3 b4 :: f a
b4             = (a -> a -> a -> a -> (a, b1, b2)
f (a -> a -> a -> a -> (a, b1, b2))
-> f a -> f (a -> a -> a -> (a, b1, b2))
forall (b :: * -> *) a a'. ExB b => (a -> a') -> b a -> b a'
/.\ f a
b1 f (a -> a -> a -> (a, b1, b2)) -> f a -> f (a -> a -> (a, b1, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b2 f (a -> a -> (a, b1, b2)) -> f a -> f (a -> (a, b1, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b3 f (a -> (a, b1, b2)) -> f a -> f (a, b1, b2)
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b4 f (a, b1, b2) -> (f a, f b1, f b2)
forall (f :: * -> *) a b1 b2.
Functor f =>
f (a, b1, b2) -> (f a, f b1, f b2)
|<<)
res53 :: (a -> a -> a -> a -> a -> (a, b1, b2))
-> f a -> f a -> f a -> f a -> f a -> (f a, f b1, f b2)
res53 f :: a -> a -> a -> a -> a -> (a, b1, b2)
f b1 :: f a
b1 b2 :: f a
b2 b3 :: f a
b3 b4 :: f a
b4 b5 :: f a
b5          = (a -> a -> a -> a -> a -> (a, b1, b2)
f (a -> a -> a -> a -> a -> (a, b1, b2))
-> f a -> f (a -> a -> a -> a -> (a, b1, b2))
forall (b :: * -> *) a a'. ExB b => (a -> a') -> b a -> b a'
/.\ f a
b1 f (a -> a -> a -> a -> (a, b1, b2))
-> f a -> f (a -> a -> a -> (a, b1, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b2 f (a -> a -> a -> (a, b1, b2)) -> f a -> f (a -> a -> (a, b1, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b3 f (a -> a -> (a, b1, b2)) -> f a -> f (a -> (a, b1, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b4 f (a -> (a, b1, b2)) -> f a -> f (a, b1, b2)
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b5 f (a, b1, b2) -> (f a, f b1, f b2)
forall (f :: * -> *) a b1 b2.
Functor f =>
f (a, b1, b2) -> (f a, f b1, f b2)
|<<)
res63 :: (a -> a -> a -> a -> a -> a -> (a, b1, b2))
-> f a -> f a -> f a -> f a -> f a -> f a -> (f a, f b1, f b2)
res63 f :: a -> a -> a -> a -> a -> a -> (a, b1, b2)
f b1 :: f a
b1 b2 :: f a
b2 b3 :: f a
b3 b4 :: f a
b4 b5 :: f a
b5 b6 :: f a
b6       = (a -> a -> a -> a -> a -> a -> (a, b1, b2)
f (a -> a -> a -> a -> a -> a -> (a, b1, b2))
-> f a -> f (a -> a -> a -> a -> a -> (a, b1, b2))
forall (b :: * -> *) a a'. ExB b => (a -> a') -> b a -> b a'
/.\ f a
b1 f (a -> a -> a -> a -> a -> (a, b1, b2))
-> f a -> f (a -> a -> a -> a -> (a, b1, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b2 f (a -> a -> a -> a -> (a, b1, b2))
-> f a -> f (a -> a -> a -> (a, b1, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b3 f (a -> a -> a -> (a, b1, b2)) -> f a -> f (a -> a -> (a, b1, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b4 f (a -> a -> (a, b1, b2)) -> f a -> f (a -> (a, b1, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b5 f (a -> (a, b1, b2)) -> f a -> f (a, b1, b2)
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b6 f (a, b1, b2) -> (f a, f b1, f b2)
forall (f :: * -> *) a b1 b2.
Functor f =>
f (a, b1, b2) -> (f a, f b1, f b2)
|<<)
res73 :: (a -> a -> a -> a -> a -> a -> a -> (a, b1, b2))
-> f a
-> f a
-> f a
-> f a
-> f a
-> f a
-> f a
-> (f a, f b1, f b2)
res73 f :: a -> a -> a -> a -> a -> a -> a -> (a, b1, b2)
f b1 :: f a
b1 b2 :: f a
b2 b3 :: f a
b3 b4 :: f a
b4 b5 :: f a
b5 b6 :: f a
b6 b7 :: f a
b7    = (a -> a -> a -> a -> a -> a -> a -> (a, b1, b2)
f (a -> a -> a -> a -> a -> a -> a -> (a, b1, b2))
-> f a -> f (a -> a -> a -> a -> a -> a -> (a, b1, b2))
forall (b :: * -> *) a a'. ExB b => (a -> a') -> b a -> b a'
/.\ f a
b1 f (a -> a -> a -> a -> a -> a -> (a, b1, b2))
-> f a -> f (a -> a -> a -> a -> a -> (a, b1, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b2 f (a -> a -> a -> a -> a -> (a, b1, b2))
-> f a -> f (a -> a -> a -> a -> (a, b1, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b3 f (a -> a -> a -> a -> (a, b1, b2))
-> f a -> f (a -> a -> a -> (a, b1, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b4 f (a -> a -> a -> (a, b1, b2)) -> f a -> f (a -> a -> (a, b1, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b5 f (a -> a -> (a, b1, b2)) -> f a -> f (a -> (a, b1, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b6 f (a -> (a, b1, b2)) -> f a -> f (a, b1, b2)
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b7 f (a, b1, b2) -> (f a, f b1, f b2)
forall (f :: * -> *) a b1 b2.
Functor f =>
f (a, b1, b2) -> (f a, f b1, f b2)
|<<)
res83 :: (a -> a -> a -> a -> a -> a -> a -> a -> (a, b1, b2))
-> f a
-> f a
-> f a
-> f a
-> f a
-> f a
-> p
-> f a
-> (f a, f b1, f b2)
res83 f :: a -> a -> a -> a -> a -> a -> a -> a -> (a, b1, b2)
f b1 :: f a
b1 b2 :: f a
b2 b3 :: f a
b3 b4 :: f a
b4 b5 :: f a
b5 b6 :: f a
b6 b7 :: p
b7 b8 :: f a
b8 = (a -> a -> a -> a -> a -> a -> a -> a -> (a, b1, b2)
f (a -> a -> a -> a -> a -> a -> a -> a -> (a, b1, b2))
-> f a -> f (a -> a -> a -> a -> a -> a -> a -> (a, b1, b2))
forall (b :: * -> *) a a'. ExB b => (a -> a') -> b a -> b a'
/.\ f a
b1 f (a -> a -> a -> a -> a -> a -> a -> (a, b1, b2))
-> f a -> f (a -> a -> a -> a -> a -> a -> (a, b1, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b2 f (a -> a -> a -> a -> a -> a -> (a, b1, b2))
-> f a -> f (a -> a -> a -> a -> a -> (a, b1, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b3 f (a -> a -> a -> a -> a -> (a, b1, b2))
-> f a -> f (a -> a -> a -> a -> (a, b1, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b4 f (a -> a -> a -> a -> (a, b1, b2))
-> f a -> f (a -> a -> a -> (a, b1, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b5 f (a -> a -> a -> (a, b1, b2)) -> f a -> f (a -> a -> (a, b1, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b6 f (a -> a -> (a, b1, b2)) -> f a -> f (a -> (a, b1, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b5 f (a -> (a, b1, b2)) -> f a -> f (a, b1, b2)
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b8 f (a, b1, b2) -> (f a, f b1, f b2)
forall (f :: * -> *) a b1 b2.
Functor f =>
f (a, b1, b2) -> (f a, f b1, f b2)
|<<)
res14 :: (a -> (a, b1, c, b2)) -> f a -> (f a, f b1, f c, f b2)
res14 f :: a -> (a, b1, c, b2)
f b1 :: f a
b1                      = (a -> (a, b1, c, b2)
f (a -> (a, b1, c, b2)) -> f a -> f (a, b1, c, b2)
forall (b :: * -> *) a a'. ExB b => (a -> a') -> b a -> b a'
/.\ f a
b1 f (a, b1, c, b2) -> (f a, f b1, f c, f b2)
forall (f :: * -> *) a b1 c b2.
Functor f =>
f (a, b1, c, b2) -> (f a, f b1, f c, f b2)
|<<<)
res24 :: (a -> a -> (a, b1, c, b2)) -> f a -> f a -> (f a, f b1, f c, f b2)
res24 f :: a -> a -> (a, b1, c, b2)
f b1 :: f a
b1 b2 :: f a
b2                   = (a -> a -> (a, b1, c, b2)
f (a -> a -> (a, b1, c, b2)) -> f a -> f (a -> (a, b1, c, b2))
forall (b :: * -> *) a a'. ExB b => (a -> a') -> b a -> b a'
/.\ f a
b1 f (a -> (a, b1, c, b2)) -> f a -> f (a, b1, c, b2)
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b2 f (a, b1, c, b2) -> (f a, f b1, f c, f b2)
forall (f :: * -> *) a b1 c b2.
Functor f =>
f (a, b1, c, b2) -> (f a, f b1, f c, f b2)
|<<<)
res34 :: (a -> a -> a -> (a, b1, c, b2))
-> f a -> f a -> f a -> (f a, f b1, f c, f b2)
res34 f :: a -> a -> a -> (a, b1, c, b2)
f b1 :: f a
b1 b2 :: f a
b2 b3 :: f a
b3                = (a -> a -> a -> (a, b1, c, b2)
f (a -> a -> a -> (a, b1, c, b2))
-> f a -> f (a -> a -> (a, b1, c, b2))
forall (b :: * -> *) a a'. ExB b => (a -> a') -> b a -> b a'
/.\ f a
b1 f (a -> a -> (a, b1, c, b2)) -> f a -> f (a -> (a, b1, c, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b2 f (a -> (a, b1, c, b2)) -> f a -> f (a, b1, c, b2)
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b3 f (a, b1, c, b2) -> (f a, f b1, f c, f b2)
forall (f :: * -> *) a b1 c b2.
Functor f =>
f (a, b1, c, b2) -> (f a, f b1, f c, f b2)
|<<<)
res44 :: (a -> a -> a -> a -> (a, b1, c, b2))
-> f a -> f a -> f a -> f a -> (f a, f b1, f c, f b2)
res44 f :: a -> a -> a -> a -> (a, b1, c, b2)
f b1 :: f a
b1 b2 :: f a
b2 b3 :: f a
b3 b4 :: f a
b4             = (a -> a -> a -> a -> (a, b1, c, b2)
f (a -> a -> a -> a -> (a, b1, c, b2))
-> f a -> f (a -> a -> a -> (a, b1, c, b2))
forall (b :: * -> *) a a'. ExB b => (a -> a') -> b a -> b a'
/.\ f a
b1 f (a -> a -> a -> (a, b1, c, b2))
-> f a -> f (a -> a -> (a, b1, c, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b2 f (a -> a -> (a, b1, c, b2)) -> f a -> f (a -> (a, b1, c, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b3 f (a -> (a, b1, c, b2)) -> f a -> f (a, b1, c, b2)
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b4 f (a, b1, c, b2) -> (f a, f b1, f c, f b2)
forall (f :: * -> *) a b1 c b2.
Functor f =>
f (a, b1, c, b2) -> (f a, f b1, f c, f b2)
|<<<)
res54 :: (a -> a -> a -> a -> a -> (a, b1, c, b2))
-> f a -> f a -> f a -> f a -> f a -> (f a, f b1, f c, f b2)
res54 f :: a -> a -> a -> a -> a -> (a, b1, c, b2)
f b1 :: f a
b1 b2 :: f a
b2 b3 :: f a
b3 b4 :: f a
b4 b5 :: f a
b5          = (a -> a -> a -> a -> a -> (a, b1, c, b2)
f (a -> a -> a -> a -> a -> (a, b1, c, b2))
-> f a -> f (a -> a -> a -> a -> (a, b1, c, b2))
forall (b :: * -> *) a a'. ExB b => (a -> a') -> b a -> b a'
/.\ f a
b1 f (a -> a -> a -> a -> (a, b1, c, b2))
-> f a -> f (a -> a -> a -> (a, b1, c, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b2 f (a -> a -> a -> (a, b1, c, b2))
-> f a -> f (a -> a -> (a, b1, c, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b3 f (a -> a -> (a, b1, c, b2)) -> f a -> f (a -> (a, b1, c, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b4 f (a -> (a, b1, c, b2)) -> f a -> f (a, b1, c, b2)
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b5 f (a, b1, c, b2) -> (f a, f b1, f c, f b2)
forall (f :: * -> *) a b1 c b2.
Functor f =>
f (a, b1, c, b2) -> (f a, f b1, f c, f b2)
|<<<)
res64 :: (a -> a -> a -> a -> a -> a -> (a, b1, c, b2))
-> f a -> f a -> f a -> f a -> f a -> f a -> (f a, f b1, f c, f b2)
res64 f :: a -> a -> a -> a -> a -> a -> (a, b1, c, b2)
f b1 :: f a
b1 b2 :: f a
b2 b3 :: f a
b3 b4 :: f a
b4 b5 :: f a
b5 b6 :: f a
b6       = (a -> a -> a -> a -> a -> a -> (a, b1, c, b2)
f (a -> a -> a -> a -> a -> a -> (a, b1, c, b2))
-> f a -> f (a -> a -> a -> a -> a -> (a, b1, c, b2))
forall (b :: * -> *) a a'. ExB b => (a -> a') -> b a -> b a'
/.\ f a
b1 f (a -> a -> a -> a -> a -> (a, b1, c, b2))
-> f a -> f (a -> a -> a -> a -> (a, b1, c, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b2 f (a -> a -> a -> a -> (a, b1, c, b2))
-> f a -> f (a -> a -> a -> (a, b1, c, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b3 f (a -> a -> a -> (a, b1, c, b2))
-> f a -> f (a -> a -> (a, b1, c, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b4 f (a -> a -> (a, b1, c, b2)) -> f a -> f (a -> (a, b1, c, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b5 f (a -> (a, b1, c, b2)) -> f a -> f (a, b1, c, b2)
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b6 f (a, b1, c, b2) -> (f a, f b1, f c, f b2)
forall (f :: * -> *) a b1 c b2.
Functor f =>
f (a, b1, c, b2) -> (f a, f b1, f c, f b2)
|<<<)
res74 :: (a -> a -> a -> a -> a -> a -> a -> (a, b1, c, b2))
-> f a
-> f a
-> f a
-> f a
-> f a
-> f a
-> f a
-> (f a, f b1, f c, f b2)
res74 f :: a -> a -> a -> a -> a -> a -> a -> (a, b1, c, b2)
f b1 :: f a
b1 b2 :: f a
b2 b3 :: f a
b3 b4 :: f a
b4 b5 :: f a
b5 b6 :: f a
b6 b7 :: f a
b7    = (a -> a -> a -> a -> a -> a -> a -> (a, b1, c, b2)
f (a -> a -> a -> a -> a -> a -> a -> (a, b1, c, b2))
-> f a -> f (a -> a -> a -> a -> a -> a -> (a, b1, c, b2))
forall (b :: * -> *) a a'. ExB b => (a -> a') -> b a -> b a'
/.\ f a
b1 f (a -> a -> a -> a -> a -> a -> (a, b1, c, b2))
-> f a -> f (a -> a -> a -> a -> a -> (a, b1, c, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b2 f (a -> a -> a -> a -> a -> (a, b1, c, b2))
-> f a -> f (a -> a -> a -> a -> (a, b1, c, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b3 f (a -> a -> a -> a -> (a, b1, c, b2))
-> f a -> f (a -> a -> a -> (a, b1, c, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b4 f (a -> a -> a -> (a, b1, c, b2))
-> f a -> f (a -> a -> (a, b1, c, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b5 f (a -> a -> (a, b1, c, b2)) -> f a -> f (a -> (a, b1, c, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b6 f (a -> (a, b1, c, b2)) -> f a -> f (a, b1, c, b2)
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b7 f (a, b1, c, b2) -> (f a, f b1, f c, f b2)
forall (f :: * -> *) a b1 c b2.
Functor f =>
f (a, b1, c, b2) -> (f a, f b1, f c, f b2)
|<<<)
res84 :: (a -> a -> a -> a -> a -> a -> a -> a -> (a, b1, c, b2))
-> f a
-> f a
-> f a
-> f a
-> f a
-> f a
-> f a
-> f a
-> (f a, f b1, f c, f b2)
res84 f :: a -> a -> a -> a -> a -> a -> a -> a -> (a, b1, c, b2)
f b1 :: f a
b1 b2 :: f a
b2 b3 :: f a
b3 b4 :: f a
b4 b5 :: f a
b5 b6 :: f a
b6 b7 :: f a
b7 b8 :: f a
b8 = (a -> a -> a -> a -> a -> a -> a -> a -> (a, b1, c, b2)
f (a -> a -> a -> a -> a -> a -> a -> a -> (a, b1, c, b2))
-> f a -> f (a -> a -> a -> a -> a -> a -> a -> (a, b1, c, b2))
forall (b :: * -> *) a a'. ExB b => (a -> a') -> b a -> b a'
/.\ f a
b1 f (a -> a -> a -> a -> a -> a -> a -> (a, b1, c, b2))
-> f a -> f (a -> a -> a -> a -> a -> a -> (a, b1, c, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b2 f (a -> a -> a -> a -> a -> a -> (a, b1, c, b2))
-> f a -> f (a -> a -> a -> a -> a -> (a, b1, c, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b3 f (a -> a -> a -> a -> a -> (a, b1, c, b2))
-> f a -> f (a -> a -> a -> a -> (a, b1, c, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b4 f (a -> a -> a -> a -> (a, b1, c, b2))
-> f a -> f (a -> a -> a -> (a, b1, c, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b5 f (a -> a -> a -> (a, b1, c, b2))
-> f a -> f (a -> a -> (a, b1, c, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b6 f (a -> a -> (a, b1, c, b2)) -> f a -> f (a -> (a, b1, c, b2))
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b7 f (a -> (a, b1, c, b2)) -> f a -> f (a, b1, c, b2)
forall (b :: * -> *) a a'. ExB b => b (a -> a') -> b a -> b a'
/*\ f a
b8 f (a, b1, c, b2) -> (f a, f b1, f c, f b2)
forall (f :: * -> *) a b1 c b2.
Functor f =>
f (a, b1, c, b2) -> (f a, f b1, f c, f b2)
|<<<)

-- | Prefix name for the prefix operator '/&\'.
filter :: b Bool -> b a -> b a
filter  p :: b Bool
p    = b Bool -> b a -> b a
forall (b :: * -> *) a. ExB b => b Bool -> b a -> b a
(/&\) b Bool
p

-- | Same as 'filter' but takes base (non-extended) values as
-- input arguments.
filter' :: Bool -> a -> b a
filter' p :: Bool
p a :: a
a  = b Bool -> b a -> b a
forall (b :: * -> *) a. ExB b => b Bool -> b a -> b a
(/&\) (Bool -> b Bool
forall (b :: * -> *) a. ExB b => a -> b a
extend Bool
p) (a -> b a
forall (b :: * -> *) a. ExB b => a -> b a
extend a
a)

-- | Prefix name for the degenerate operator '/!\'.
degen :: a -> b a -> a
degen a :: a
a = a -> b a -> a
forall (b :: * -> *) a. ExB b => a -> b a -> a
(/!\) a
a

-- | 
-- <<fig/eqs-exb-pattern-ignore.png>>
--
-- The @ignoreXY@ pattern takes a function of @Y + X@ arguments, @Y@
-- basic inputs followed by @X@ behavior-extended inputs. The function
-- is first lifted and applied on the @X@ behavior-extended arguments,
-- and the result is then degenerated using the @Y@ non-extended
-- arguments as fallback. The effect is similar to "ignoring" a the
-- result of a function evaluation if \(\in b\).
--
-- The main application of this pattern is as extended behavior
-- wrapper for stateful processes which do not "understand" extended
-- behavior semantics, i.e. it simply propagates the current state
-- \((\in \alpha)\) if the inputs belongs to the set of extended
-- values \((\in b)\).
--
-- Constructors: @ignore[1-4][1-4]@.
ignore22 :: ExB b
         => (a1 -> a2 -> a1' -> a2' -> (a1, a2))
         -- ^ function of @Y + X@ arguments
         -> a1 -> a2 -> b a1' -> b a2' -> (a1, a2)
     
ignore11 :: (t -> a -> t) -> t -> b a -> t
ignore11 f :: t -> a -> t
f a1 :: t
a1 b1 :: b a
b1          = t -> b t -> t
forall (b :: * -> *) a. ExB b => a -> b a -> a
degen t
a1 (b t -> t) -> b t -> t
forall a b. (a -> b) -> a -> b
$ (a -> t) -> b a -> b t
forall (b :: * -> *) a a'. ExB b => (a -> a') -> b a -> b a'
res11 (t -> a -> t
f t
a1) b a
b1
ignore21 :: (t -> a -> a -> t) -> t -> b a -> b a -> t
ignore21 f :: t -> a -> a -> t
f a1 :: t
a1 b1 :: b a
b1 b2 :: b a
b2       = t -> b t -> t
forall (b :: * -> *) a. ExB b => a -> b a -> a
degen t
a1 (b t -> t) -> b t -> t
forall a b. (a -> b) -> a -> b
$ (a -> a -> t) -> b a -> b a -> b t
forall (b :: * -> *) a a a'.
ExB b =>
(a -> a -> a') -> b a -> b a -> b a'
res21 (t -> a -> a -> t
f t
a1) b a
b1 b a
b2
ignore31 :: (t -> a -> a -> a -> t) -> t -> b a -> b a -> b a -> t
ignore31 f :: t -> a -> a -> a -> t
f a1 :: t
a1 b1 :: b a
b1 b2 :: b a
b2 b3 :: b a
b3    = t -> b t -> t
forall (b :: * -> *) a. ExB b => a -> b a -> a
degen t
a1 (b t -> t) -> b t -> t
forall a b. (a -> b) -> a -> b
$ (a -> a -> a -> t) -> b a -> b a -> b a -> b t
forall (b :: * -> *) a a a a'.
ExB b =>
(a -> a -> a -> a') -> b a -> b a -> b a -> b a'
res31 (t -> a -> a -> a -> t
f t
a1) b a
b1 b a
b2 b a
b3
ignore41 :: (t -> a -> a -> a -> a -> t) -> t -> b a -> b a -> b a -> b a -> t
ignore41 f :: t -> a -> a -> a -> a -> t
f a1 :: t
a1 b1 :: b a
b1 b2 :: b a
b2 b3 :: b a
b3 b4 :: b a
b4 = t -> b t -> t
forall (b :: * -> *) a. ExB b => a -> b a -> a
degen t
a1 (b t -> t) -> b t -> t
forall a b. (a -> b) -> a -> b
$ (a -> a -> a -> a -> t) -> b a -> b a -> b a -> b a -> b t
forall (b :: * -> *) a a a a a'.
ExB b =>
(a -> a -> a -> a -> a') -> b a -> b a -> b a -> b a -> b a'
res41 (t -> a -> a -> a -> a -> t
f t
a1) b a
b1 b a
b2 b a
b3 b a
b4
ignore12 :: (t -> t -> a -> (t, t)) -> t -> t -> b a -> (t, t)
ignore12 f :: t -> t -> a -> (t, t)
f a1 :: t
a1 a2 :: t
a2 b1 :: b a
b1          = (t, t) -> b (t, t) -> (t, t)
forall (b :: * -> *) a. ExB b => a -> b a -> a
degen (t
a1, t
a2) (b (t, t) -> (t, t)) -> b (t, t) -> (t, t)
forall a b. (a -> b) -> a -> b
$ (a -> (t, t)) -> b a -> b (t, t)
forall (b :: * -> *) a a'. ExB b => (a -> a') -> b a -> b a'
res11 (t -> t -> a -> (t, t)
f t
a1 t
a2) b a
b1
ignore22 :: (a1 -> a2 -> a1' -> a2' -> (a1, a2))
-> a1 -> a2 -> b a1' -> b a2' -> (a1, a2)
ignore22 f :: a1 -> a2 -> a1' -> a2' -> (a1, a2)
f a1 :: a1
a1 a2 :: a2
a2 b1 :: b a1'
b1 b2 :: b a2'
b2       = (a1, a2) -> b (a1, a2) -> (a1, a2)
forall (b :: * -> *) a. ExB b => a -> b a -> a
degen (a1
a1, a2
a2) (b (a1, a2) -> (a1, a2)) -> b (a1, a2) -> (a1, a2)
forall a b. (a -> b) -> a -> b
$ (a1' -> a2' -> (a1, a2)) -> b a1' -> b a2' -> b (a1, a2)
forall (b :: * -> *) a a a'.
ExB b =>
(a -> a -> a') -> b a -> b a -> b a'
res21 (a1 -> a2 -> a1' -> a2' -> (a1, a2)
f a1
a1 a2
a2) b a1'
b1 b a2'
b2
ignore32 :: (t -> t -> a -> a -> a -> (t, t))
-> t -> t -> b a -> b a -> b a -> (t, t)
ignore32 f :: t -> t -> a -> a -> a -> (t, t)
f a1 :: t
a1 a2 :: t
a2 b1 :: b a
b1 b2 :: b a
b2 b3 :: b a
b3    = (t, t) -> b (t, t) -> (t, t)
forall (b :: * -> *) a. ExB b => a -> b a -> a
degen (t
a1, t
a2) (b (t, t) -> (t, t)) -> b (t, t) -> (t, t)
forall a b. (a -> b) -> a -> b
$ (a -> a -> a -> (t, t)) -> b a -> b a -> b a -> b (t, t)
forall (b :: * -> *) a a a a'.
ExB b =>
(a -> a -> a -> a') -> b a -> b a -> b a -> b a'
res31 (t -> t -> a -> a -> a -> (t, t)
f t
a1 t
a2) b a
b1 b a
b2 b a
b3
ignore42 :: (t -> t -> a -> a -> a -> a -> (t, t))
-> t -> t -> b a -> b a -> b a -> b a -> (t, t)
ignore42 f :: t -> t -> a -> a -> a -> a -> (t, t)
f a1 :: t
a1 a2 :: t
a2 b1 :: b a
b1 b2 :: b a
b2 b3 :: b a
b3 b4 :: b a
b4 = (t, t) -> b (t, t) -> (t, t)
forall (b :: * -> *) a. ExB b => a -> b a -> a
degen (t
a1, t
a2) (b (t, t) -> (t, t)) -> b (t, t) -> (t, t)
forall a b. (a -> b) -> a -> b
$ (a -> a -> a -> a -> (t, t))
-> b a -> b a -> b a -> b a -> b (t, t)
forall (b :: * -> *) a a a a a'.
ExB b =>
(a -> a -> a -> a -> a') -> b a -> b a -> b a -> b a -> b a'
res41 (t -> t -> a -> a -> a -> a -> (t, t)
f t
a1 t
a2) b a
b1 b a
b2 b a
b3 b a
b4
ignore13 :: (t -> t -> t -> a -> (t, t, t)) -> t -> t -> t -> b a -> (t, t, t)
ignore13 f :: t -> t -> t -> a -> (t, t, t)
f a1 :: t
a1 a2 :: t
a2 a3 :: t
a3 b1 :: b a
b1          = (t, t, t) -> b (t, t, t) -> (t, t, t)
forall (b :: * -> *) a. ExB b => a -> b a -> a
degen (t
a1, t
a2, t
a3) (b (t, t, t) -> (t, t, t)) -> b (t, t, t) -> (t, t, t)
forall a b. (a -> b) -> a -> b
$ (a -> (t, t, t)) -> b a -> b (t, t, t)
forall (b :: * -> *) a a'. ExB b => (a -> a') -> b a -> b a'
res11 (t -> t -> t -> a -> (t, t, t)
f t
a1 t
a2 t
a3) b a
b1
ignore23 :: (t -> t -> t -> a -> a -> (t, t, t))
-> t -> t -> t -> b a -> b a -> (t, t, t)
ignore23 f :: t -> t -> t -> a -> a -> (t, t, t)
f a1 :: t
a1 a2 :: t
a2 a3 :: t
a3 b1 :: b a
b1 b2 :: b a
b2       = (t, t, t) -> b (t, t, t) -> (t, t, t)
forall (b :: * -> *) a. ExB b => a -> b a -> a
degen (t
a1, t
a2, t
a3) (b (t, t, t) -> (t, t, t)) -> b (t, t, t) -> (t, t, t)
forall a b. (a -> b) -> a -> b
$ (a -> a -> (t, t, t)) -> b a -> b a -> b (t, t, t)
forall (b :: * -> *) a a a'.
ExB b =>
(a -> a -> a') -> b a -> b a -> b a'
res21 (t -> t -> t -> a -> a -> (t, t, t)
f t
a1 t
a2 t
a3) b a
b1 b a
b2
ignore33 :: (t -> t -> t -> a -> a -> a -> (t, t, t))
-> t -> t -> t -> b a -> b a -> b a -> (t, t, t)
ignore33 f :: t -> t -> t -> a -> a -> a -> (t, t, t)
f a1 :: t
a1 a2 :: t
a2 a3 :: t
a3 b1 :: b a
b1 b2 :: b a
b2 b3 :: b a
b3    = (t, t, t) -> b (t, t, t) -> (t, t, t)
forall (b :: * -> *) a. ExB b => a -> b a -> a
degen (t
a1, t
a2, t
a3) (b (t, t, t) -> (t, t, t)) -> b (t, t, t) -> (t, t, t)
forall a b. (a -> b) -> a -> b
$ (a -> a -> a -> (t, t, t)) -> b a -> b a -> b a -> b (t, t, t)
forall (b :: * -> *) a a a a'.
ExB b =>
(a -> a -> a -> a') -> b a -> b a -> b a -> b a'
res31 (t -> t -> t -> a -> a -> a -> (t, t, t)
f t
a1 t
a2 t
a3) b a
b1 b a
b2 b a
b3
ignore43 :: (t -> t -> t -> a -> a -> a -> a -> (t, t, t))
-> t -> t -> t -> b a -> b a -> b a -> b a -> (t, t, t)
ignore43 f :: t -> t -> t -> a -> a -> a -> a -> (t, t, t)
f a1 :: t
a1 a2 :: t
a2 a3 :: t
a3 b1 :: b a
b1 b2 :: b a
b2 b3 :: b a
b3 b4 :: b a
b4 = (t, t, t) -> b (t, t, t) -> (t, t, t)
forall (b :: * -> *) a. ExB b => a -> b a -> a
degen (t
a1, t
a2, t
a3) (b (t, t, t) -> (t, t, t)) -> b (t, t, t) -> (t, t, t)
forall a b. (a -> b) -> a -> b
$ (a -> a -> a -> a -> (t, t, t))
-> b a -> b a -> b a -> b a -> b (t, t, t)
forall (b :: * -> *) a a a a a'.
ExB b =>
(a -> a -> a -> a -> a') -> b a -> b a -> b a -> b a -> b a'
res41 (t -> t -> t -> a -> a -> a -> a -> (t, t, t)
f t
a1 t
a2 t
a3) b a
b1 b a
b2 b a
b3 b a
b4
ignore14 :: (t -> t -> t -> t -> a -> (t, t, t, t))
-> t -> t -> t -> t -> b a -> (t, t, t, t)
ignore14 f :: t -> t -> t -> t -> a -> (t, t, t, t)
f a1 :: t
a1 a2 :: t
a2 a3 :: t
a3 a4 :: t
a4 b1 :: b a
b1          = (t, t, t, t) -> b (t, t, t, t) -> (t, t, t, t)
forall (b :: * -> *) a. ExB b => a -> b a -> a
degen (t
a1, t
a2, t
a3, t
a4) (b (t, t, t, t) -> (t, t, t, t)) -> b (t, t, t, t) -> (t, t, t, t)
forall a b. (a -> b) -> a -> b
$ (a -> (t, t, t, t)) -> b a -> b (t, t, t, t)
forall (b :: * -> *) a a'. ExB b => (a -> a') -> b a -> b a'
res11 (t -> t -> t -> t -> a -> (t, t, t, t)
f t
a1 t
a2 t
a3 t
a4) b a
b1
ignore24 :: (t -> t -> t -> t -> a -> a -> (t, t, t, t))
-> t -> t -> t -> t -> b a -> b a -> (t, t, t, t)
ignore24 f :: t -> t -> t -> t -> a -> a -> (t, t, t, t)
f a1 :: t
a1 a2 :: t
a2 a3 :: t
a3 a4 :: t
a4 b1 :: b a
b1 b2 :: b a
b2       = (t, t, t, t) -> b (t, t, t, t) -> (t, t, t, t)
forall (b :: * -> *) a. ExB b => a -> b a -> a
degen (t
a1, t
a2, t
a3, t
a4) (b (t, t, t, t) -> (t, t, t, t)) -> b (t, t, t, t) -> (t, t, t, t)
forall a b. (a -> b) -> a -> b
$ (a -> a -> (t, t, t, t)) -> b a -> b a -> b (t, t, t, t)
forall (b :: * -> *) a a a'.
ExB b =>
(a -> a -> a') -> b a -> b a -> b a'
res21 (t -> t -> t -> t -> a -> a -> (t, t, t, t)
f t
a1 t
a2 t
a3 t
a4) b a
b1 b a
b2
ignore34 :: (t -> t -> t -> t -> a -> a -> a -> (t, t, t, t))
-> t -> t -> t -> t -> b a -> b a -> b a -> (t, t, t, t)
ignore34 f :: t -> t -> t -> t -> a -> a -> a -> (t, t, t, t)
f a1 :: t
a1 a2 :: t
a2 a3 :: t
a3 a4 :: t
a4 b1 :: b a
b1 b2 :: b a
b2 b3 :: b a
b3    = (t, t, t, t) -> b (t, t, t, t) -> (t, t, t, t)
forall (b :: * -> *) a. ExB b => a -> b a -> a
degen (t
a1, t
a2, t
a3, t
a4) (b (t, t, t, t) -> (t, t, t, t)) -> b (t, t, t, t) -> (t, t, t, t)
forall a b. (a -> b) -> a -> b
$ (a -> a -> a -> (t, t, t, t))
-> b a -> b a -> b a -> b (t, t, t, t)
forall (b :: * -> *) a a a a'.
ExB b =>
(a -> a -> a -> a') -> b a -> b a -> b a -> b a'
res31 (t -> t -> t -> t -> a -> a -> a -> (t, t, t, t)
f t
a1 t
a2 t
a3 t
a4) b a
b1 b a
b2 b a
b3
ignore44 :: (t -> t -> t -> t -> a -> a -> a -> a -> (t, t, t, t))
-> t -> t -> t -> t -> b a -> b a -> b a -> b a -> (t, t, t, t)
ignore44 f :: t -> t -> t -> t -> a -> a -> a -> a -> (t, t, t, t)
f a1 :: t
a1 a2 :: t
a2 a3 :: t
a3 a4 :: t
a4 b1 :: b a
b1 b2 :: b a
b2 b3 :: b a
b3 b4 :: b a
b4 = (t, t, t, t) -> b (t, t, t, t) -> (t, t, t, t)
forall (b :: * -> *) a. ExB b => a -> b a -> a
degen (t
a1, t
a2, t
a3, t
a4) (b (t, t, t, t) -> (t, t, t, t)) -> b (t, t, t, t) -> (t, t, t, t)
forall a b. (a -> b) -> a -> b
$ (a -> a -> a -> a -> (t, t, t, t))
-> b a -> b a -> b a -> b a -> b (t, t, t, t)
forall (b :: * -> *) a a a a a'.
ExB b =>
(a -> a -> a -> a -> a') -> b a -> b a -> b a -> b a -> b a'
res41 (t -> t -> t -> t -> a -> a -> a -> a -> (t, t, t, t)
f t
a1 t
a2 t
a3 t
a4) b a
b1 b a
b2 b a
b3 b a
b4