{-# LANGUAGE DeriveFunctor       #-}
{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications    #-}

-- SPDX-License-Identifier: BSD-3-Clause

-----------------------------------------------------------------------------
-- |
-- Module      :  Data.ProEnumeration
-- Copyright   :  Brent Yorgey, Koji Miyazato
-- Maintainer  :  byorgey@gmail.com
--
-- A /proenumeration/ is a pair of a 'CoEnumeration' and an 'Enumeration'
-- sharing the same cardinality.
--
-- A /proenumeration/ can be seen as a function with an explicitly enumerated
-- range.
--
-- Through documentations of this module, these import aliases are used:
--
-- > import qualified Data.Enumeration as E
-- > import qualified Data.CoEnumeration as C

-----------------------------------------------------------------------------

module Data.ProEnumeration(
  -- * Proenumeration type
    ProEnumeration()
  , card, select, locate

  , isFinite
  , baseEnum, baseCoEnum, run
  , enumerateRange

  , unsafeMkProEnumeration
  , mkProEnumeration

  -- * ProEnumeration is a Profunctor
  , dimap, (.@), (@.)

  -- * Using Cardinality
  , Cardinality(..), Index

  -- * Primitive proenumerations
  , unit, empty
  , singleton
  , modulo, clamped, boundsChecked
  , finiteList, finiteCycle
  , boundedEnum
  , nat, int, cw, rat

  -- * Combinators
  , infinite
  , compose
  , (><), (<+>)
  , maybeOf, eitherOf
  , listOf, finiteSubsetOf

  , enumerateP, coenumerateP
  , proenumerationOf
  , finiteFunctionOf
) where

import qualified Control.Applicative        as Ap (Alternative (empty))
import           Data.Void

import           Data.Functor.Contravariant

import           Data.CoEnumeration         (CoEnumeration)
import qualified Data.CoEnumeration         as C
import           Data.Enumeration           (Cardinality (..), Enumeration,
                                             Index)
import qualified Data.Enumeration           as E

-- | A /proenumeration/ is a pair of a 'CoEnumeration' and an 'Enumeration'
-- sharing the same cardinality.
-- Alternatively, a /proenumeration/ can be seen as a function with an
-- explicitly enumerated range.
--
-- Through this documentation,
-- proenumerations are shown in diagrams of the following shape:
--
-- >    f      g
-- > a ---> N ---> b  :: ProEnumeration a b
--
-- Which means it is a value @p :: ProEnumeration a b@ with
-- cardinality @N@, @locate p = f@, and @select p = g@.
--
-- We can see @N@ in the diagram as a subset of integers:
--
-- > N = {i :: Integer | i < N}
--
-- Then it is actually a (category-theoretic)
-- diagram showing values of @ProEnumeration a b@.
data ProEnumeration a b =
  ProEnumeration {
    -- | Get the cardinality of a proenumeration
    forall a b. ProEnumeration a b -> Cardinality
card   :: Cardinality

    -- | See @E.'E.select'@
  , forall a b. ProEnumeration a b -> Integer -> b
select :: Index -> b

    -- | See @C.'C.locate'@
  , forall a b. ProEnumeration a b -> a -> Integer
locate :: a -> Index
  }
  deriving ((forall a b. (a -> b) -> ProEnumeration a a -> ProEnumeration a b)
-> (forall a b. a -> ProEnumeration a b -> ProEnumeration a a)
-> Functor (ProEnumeration a)
forall a b. a -> ProEnumeration a b -> ProEnumeration a a
forall a b. (a -> b) -> ProEnumeration a a -> ProEnumeration a b
forall a a b. a -> ProEnumeration a b -> ProEnumeration a a
forall a a b. (a -> b) -> ProEnumeration a a -> ProEnumeration a b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a a b. (a -> b) -> ProEnumeration a a -> ProEnumeration a b
fmap :: forall a b. (a -> b) -> ProEnumeration a a -> ProEnumeration a b
$c<$ :: forall a a b. a -> ProEnumeration a b -> ProEnumeration a a
<$ :: forall a b. a -> ProEnumeration a b -> ProEnumeration a a
Functor)

-- | Returns if the the cardinality of a proenumeration is finite.
isFinite :: ProEnumeration a b -> Bool
isFinite :: forall a b. ProEnumeration a b -> Bool
isFinite = (Cardinality -> Cardinality -> Bool
forall a. Eq a => a -> a -> Bool
/= Cardinality
Infinite) (Cardinality -> Bool)
-> (ProEnumeration a b -> Cardinality)
-> ProEnumeration a b
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProEnumeration a b -> Cardinality
forall a b. ProEnumeration a b -> Cardinality
card

-- | ProEnumeration is a Profunctor
--
-- > dimap l r p = l .@ p @. r
dimap :: (a' -> a) -> (b -> b') -> ProEnumeration a b -> ProEnumeration a' b'
dimap :: forall a' a b b'.
(a' -> a)
-> (b -> b') -> ProEnumeration a b -> ProEnumeration a' b'
dimap a' -> a
l b -> b'
r ProEnumeration a b
p = ProEnumeration a b
p{ select = r . select p, locate = locate p . l }

-- | > p @. r = dimap id r p
(@.) :: ProEnumeration a b -> (b -> b') -> ProEnumeration a b'
@. :: forall a b b'.
ProEnumeration a b -> (b -> b') -> ProEnumeration a b'
(@.) = ((b -> b') -> ProEnumeration a b -> ProEnumeration a b')
-> ProEnumeration a b -> (b -> b') -> ProEnumeration a b'
forall a b c. (a -> b -> c) -> b -> a -> c
flip (b -> b') -> ProEnumeration a b -> ProEnumeration a b'
forall a b. (a -> b) -> ProEnumeration a a -> ProEnumeration a b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap

infixl 7 @.

-- | > l .@ p = dimap l id p
(.@) :: (a' -> a) -> ProEnumeration a b -> ProEnumeration a' b
a' -> a
l .@ :: forall a' a b.
(a' -> a) -> ProEnumeration a b -> ProEnumeration a' b
.@ ProEnumeration a b
p = ProEnumeration a b
p{ locate = locate p . l }

infixr 8 .@

-- | Take an 'Enumeration' from a proenumeration,
--   discarding the @CoEnumeration@ part
baseEnum :: ProEnumeration a b -> Enumeration b
baseEnum :: forall a b. ProEnumeration a b -> Enumeration b
baseEnum ProEnumeration a b
p = Cardinality -> (Integer -> b) -> Enumeration b
forall a. Cardinality -> (Integer -> a) -> Enumeration a
E.mkEnumeration (ProEnumeration a b -> Cardinality
forall a b. ProEnumeration a b -> Cardinality
card ProEnumeration a b
p) (ProEnumeration a b -> Integer -> b
forall a b. ProEnumeration a b -> Integer -> b
select ProEnumeration a b
p)

-- | Take an 'CoEnumeration' from a proenumeration,
--   discarding @Enumeration@ part
baseCoEnum :: ProEnumeration a b -> CoEnumeration a
baseCoEnum :: forall a b. ProEnumeration a b -> CoEnumeration a
baseCoEnum ProEnumeration a b
p = Cardinality -> (a -> Integer) -> CoEnumeration a
forall a. Cardinality -> (a -> Integer) -> CoEnumeration a
C.unsafeMkCoEnumeration (ProEnumeration a b -> Cardinality
forall a b. ProEnumeration a b -> Cardinality
card ProEnumeration a b
p) (ProEnumeration a b -> a -> Integer
forall a b. ProEnumeration a b -> a -> Integer
locate ProEnumeration a b
p)

-- | Turn a proenumeration into a normal function.
--
-- > run p = (select p :: Index -> b) . (locate p :: a -> Index)
run :: ProEnumeration a b -> a -> b
run :: forall a b. ProEnumeration a b -> a -> b
run ProEnumeration a b
p = ProEnumeration a b -> Integer -> b
forall a b. ProEnumeration a b -> Integer -> b
select ProEnumeration a b
p (Integer -> b) -> (a -> Integer) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProEnumeration a b -> a -> Integer
forall a b. ProEnumeration a b -> a -> Integer
locate ProEnumeration a b
p

-- * Primitive proenumerations

-- | @enumerateRange = E.enumerate . 'baseEnum'@
enumerateRange :: ProEnumeration a b -> [b]
enumerateRange :: forall a b. ProEnumeration a b -> [b]
enumerateRange = Enumeration b -> [b]
forall a. Enumeration a -> [a]
E.enumerate (Enumeration b -> [b])
-> (ProEnumeration a b -> Enumeration b)
-> ProEnumeration a b
-> [b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProEnumeration a b -> Enumeration b
forall a b. ProEnumeration a b -> Enumeration b
baseEnum

-- | Constructs a proenumeration from a 'CoEnumeration' and an 'Enumeration'.
--
--   The cardinalities of the two arguments must be equal.
--   Otherwise, 'mkProEnumeration' returns an error.
--
--   > baseEnum (mkProEnumeration a b) = b
--   > baseCoEnum (mkProEnumeration a b) = a
--
-- >>> p = mkProEnumeration (C.modulo 3) (E.finiteList "abc")
-- >>> (card p, locate p 4, select p 1)
-- (Finite 3,1,'b')
mkProEnumeration :: CoEnumeration a -> Enumeration b -> ProEnumeration a b
mkProEnumeration :: forall a b. CoEnumeration a -> Enumeration b -> ProEnumeration a b
mkProEnumeration CoEnumeration a
a Enumeration b
b
  | Cardinality
na Cardinality -> Cardinality -> Bool
forall a. Eq a => a -> a -> Bool
== Cardinality
nb  = ProEnumeration a b
p
  | Bool
otherwise = [Char] -> ProEnumeration a b
forall a. HasCallStack => [Char] -> a
error ([Char] -> ProEnumeration a b) -> [Char] -> ProEnumeration a b
forall a b. (a -> b) -> a -> b
$ [Char]
"mkProEnumeration cardinality mismatch:" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Cardinality, Cardinality) -> [Char]
forall a. Show a => a -> [Char]
show (Cardinality
na, Cardinality
nb)
  where
    na :: Cardinality
na = CoEnumeration a -> Cardinality
forall a. CoEnumeration a -> Cardinality
C.card CoEnumeration a
a
    nb :: Cardinality
nb = Enumeration b -> Cardinality
forall a. Enumeration a -> Cardinality
E.card Enumeration b
b
    p :: ProEnumeration a b
p = ProEnumeration{ card :: Cardinality
card = Cardinality
na, select :: Integer -> b
select = Enumeration b -> Integer -> b
forall a. Enumeration a -> Integer -> a
E.select Enumeration b
b, locate :: a -> Integer
locate = CoEnumeration a -> a -> Integer
forall a. CoEnumeration a -> a -> Integer
C.locate CoEnumeration a
a }

-- | Constructs a proenumeration.
--
--   To construct a valid proenumeration by @unsafeMkProEnumeration n f g@,
--   it must satisfy the following conditions:
--
--   * For all @i :: Integer@, if @0 <= i && i < n@, then @f i@ should be
--     \"valid\" (usually, it means @f i@ should evaluate without exception).
--   * For all @x :: a@, @(Finite (g x) < n)@.
--
--   This functions does not (and never could) check the validity
--   of its arguments.
unsafeMkProEnumeration
  :: Cardinality-> (Index -> b) -> (a -> Index) -> ProEnumeration a b
unsafeMkProEnumeration :: forall b a.
Cardinality
-> (Integer -> b) -> (a -> Integer) -> ProEnumeration a b
unsafeMkProEnumeration = Cardinality
-> (Integer -> b) -> (a -> Integer) -> ProEnumeration a b
forall a b.
Cardinality
-> (Integer -> b) -> (a -> Integer) -> ProEnumeration a b
ProEnumeration

-- | @unit = 'mkProEnumeration' C.'C.unit' E.'E.unit'@
unit :: ProEnumeration a ()
unit :: forall a. ProEnumeration a ()
unit = CoEnumeration a -> Enumeration () -> ProEnumeration a ()
forall a b. CoEnumeration a -> Enumeration b -> ProEnumeration a b
mkProEnumeration CoEnumeration a
forall a. CoEnumeration a
C.unit Enumeration ()
E.unit

-- | @singleton b = b <$ 'unit' = 'mkProEnumeration' C.'C.unit' (E.'E.singleton' b)@
singleton :: b -> ProEnumeration a b
singleton :: forall b a. b -> ProEnumeration a b
singleton b
b = CoEnumeration a -> Enumeration b -> ProEnumeration a b
forall a b. CoEnumeration a -> Enumeration b -> ProEnumeration a b
mkProEnumeration CoEnumeration a
forall a. CoEnumeration a
C.unit (b -> Enumeration b
forall a. a -> Enumeration a
E.singleton b
b)

-- | @empty = 'mkProEnumeration' 'lost' 'Ap.empty'@
empty :: ProEnumeration Void b
empty :: forall b. ProEnumeration Void b
empty = CoEnumeration Void -> Enumeration b -> ProEnumeration Void b
forall a b. CoEnumeration a -> Enumeration b -> ProEnumeration a b
mkProEnumeration CoEnumeration Void
forall (f :: * -> *). Decidable f => f Void
C.lost Enumeration b
forall a. Enumeration a
forall (f :: * -> *) a. Alternative f => f a
Ap.empty

-- | @boundedEnum = 'mkProEnumeration' C.'C.boundedEnum' E.'E.boundedEnum'@
boundedEnum :: (Enum a, Bounded a) => ProEnumeration a a
boundedEnum :: forall a. (Enum a, Bounded a) => ProEnumeration a a
boundedEnum = CoEnumeration a -> Enumeration a -> ProEnumeration a a
forall a b. CoEnumeration a -> Enumeration b -> ProEnumeration a b
mkProEnumeration CoEnumeration a
forall a. (Enum a, Bounded a) => CoEnumeration a
C.boundedEnum Enumeration a
forall a. (Enum a, Bounded a) => Enumeration a
E.boundedEnum

-- | @modulo k = 'mkProEnumeration' (C.'C.modulo' k) (E.'E.finite' k)@
--
-- >>> card (modulo 13) == Finite 13
-- True
-- >>> run (modulo 13) 1462325 == 1462325 `mod` 13
-- True
modulo :: Integer -> ProEnumeration Integer Integer
modulo :: Integer -> ProEnumeration Integer Integer
modulo Integer
k = CoEnumeration Integer
-> Enumeration Integer -> ProEnumeration Integer Integer
forall a b. CoEnumeration a -> Enumeration b -> ProEnumeration a b
mkProEnumeration (Integer -> CoEnumeration Integer
C.modulo Integer
k) (Integer -> Enumeration Integer
E.finite Integer
k)

-- | @clamped lo hi@ is a proenumeration of integers,
--   which does not modify integers between @lo@ and @hi@, inclusive,
--   and limits smaller (larger) integer to @lo@ (@hi@).
--
--   It is an error to call this function if @lo > hi@.
--
--   > run (clamped lo hi) = min hi . max lo
--
-- >>> card (clamped (-2) 2)
-- Finite 5
-- >>> enumerateRange (clamped (-2) 2)
-- [-2,-1,0,1,2]
-- >>> run (clamped (-2) 2) <$> [-4 .. 4]
-- [-2,-2,-2,-1,0,1,2,2,2]
clamped :: Integer -> Integer -> ProEnumeration Integer Integer
clamped :: Integer -> Integer -> ProEnumeration Integer Integer
clamped Integer
lo Integer
hi
  | Integer
lo Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
hi = ProEnumeration
      { card :: Cardinality
card = Integer -> Cardinality
Finite (Integer
1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
hi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
lo)
      , select :: Integer -> Integer
select = (Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
lo)
      , locate :: Integer -> Integer
locate = \Integer
i -> Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min (Integer
hi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
lo) (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
0 (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
lo))
      }
  | Bool
otherwise = [Char] -> ProEnumeration Integer Integer
forall a. HasCallStack => [Char] -> a
error [Char]
"Empty range"

-- | @boundsChecked lo hi@ is a proenumeration of a \"bounds check\" function,
--   which validates that an input is between @lo@ and @hi@, inclusive,
--   and returns @Nothing@ if it is outside those bounds.
--
--   > run (boundsChecked lo hi) i
--       | lo <= i && i <= hi = Just i
--       | otherwise          = Nothing
--
-- >>> card (boundsChecked (-2) 2)
-- Finite 6
-- >>> -- Justs of [-2 .. 2] and Nothing
-- >>> enumerateRange (boundsChecked (-2) 2)
-- [Just (-2),Just (-1),Just 0,Just 1,Just 2,Nothing]
-- >>> run (boundsChecked (-2) 2) <$> [-4 .. 4]
-- [Nothing,Nothing,Just (-2),Just (-1),Just 0,Just 1,Just 2,Nothing,Nothing]
boundsChecked :: Integer -> Integer -> ProEnumeration Integer (Maybe Integer)
boundsChecked :: Integer -> Integer -> ProEnumeration Integer (Maybe Integer)
boundsChecked Integer
lo Integer
hi = ProEnumeration
  { card :: Cardinality
card = Integer -> Cardinality
Finite Integer
size
  , select :: Integer -> Maybe Integer
select = Integer -> Maybe Integer
sel
  , locate :: Integer -> Integer
locate = Integer -> Integer
loc
  }
  where
    n :: Integer
n = Integer
1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
hi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
lo
    size :: Integer
size = Integer
1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
0 Integer
n
    sel :: Integer -> Maybe Integer
sel Integer
i
      | Integer
0 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
i Bool -> Bool -> Bool
&& Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
n = Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
lo)
      | Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
n          = Maybe Integer
forall a. Maybe a
Nothing
      | Bool
otherwise = [Char] -> Maybe Integer
forall a. HasCallStack => [Char] -> a
error [Char]
"out of bounds"
    loc :: Integer -> Integer
loc Integer
k | Integer
lo Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
k Bool -> Bool -> Bool
&& Integer
k Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
hi = Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
lo
          | Bool
otherwise          = Integer
n


-- | @finiteList as@ is a proenumeration of a \"bounds checked\"
--   indexing of @as@.
--
--   > run (finiteList as) i
--       | 0 <= i && i < length as = Just (as !! i)
--       | otherwise               = Nothing
--
--   Note that 'finiteList' uses '!!' on the input list
--   under the hood, which has bad performance for long lists.
--   See also the documentation of Data.Enumeration.'E.finiteList'.
-- >>> card (finiteList "HELLO")
-- Finite 6
-- >>> -- Justs and Nothing
-- >>> enumerateRange (finiteList "HELLO")
-- [Just 'H',Just 'E',Just 'L',Just 'L',Just 'O',Nothing]
-- >>> run (finiteList "HELLO") <$> [0 .. 6]
-- [Just 'H',Just 'E',Just 'L',Just 'L',Just 'O',Nothing,Nothing]
finiteList :: [a] -> ProEnumeration Integer (Maybe a)
finiteList :: forall a. [a] -> ProEnumeration Integer (Maybe a)
finiteList [a]
as = Integer -> Integer -> ProEnumeration Integer (Maybe Integer)
boundsChecked Integer
0 (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1) ProEnumeration Integer (Maybe Integer)
-> (Maybe Integer -> Maybe a) -> ProEnumeration Integer (Maybe a)
forall a b b'.
ProEnumeration a b -> (b -> b') -> ProEnumeration a b'
@. ((Integer -> a) -> Maybe Integer -> Maybe a
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Integer -> a
sel)
  where
    as' :: Enumeration a
as' = [a] -> Enumeration a
forall a. [a] -> Enumeration a
E.finiteList [a]
as
    Finite Integer
n = Enumeration a -> Cardinality
forall a. Enumeration a -> Cardinality
E.card Enumeration a
as'
    sel :: Integer -> a
sel = Enumeration a -> Integer -> a
forall a. Enumeration a -> Integer -> a
E.select Enumeration a
as'

-- | @finiteCycle as@ is a proenumeration of an indexing of @as@,
--   where every integer is a valid index by taking it modulo @length as@.
--
--   > run (finiteCycle as) i = as !! (i `mod` length as)
--
--   If @as@ is an empty list, it is an error.
--
-- >>> card (finiteCycle "HELLO")
-- Finite 5
-- >>> enumerateRange (finiteCycle "HELLO")
-- "HELLO"
-- >>> run (finiteCycle "HELLO") <$> [0 .. 10]
-- "HELLOHELLOH"
finiteCycle :: [a] -> ProEnumeration Integer a
finiteCycle :: forall a. [a] -> ProEnumeration Integer a
finiteCycle [a]
as = Integer -> ProEnumeration Integer Integer
modulo Integer
n ProEnumeration Integer Integer
-> (Integer -> a) -> ProEnumeration Integer a
forall a b b'.
ProEnumeration a b -> (b -> b') -> ProEnumeration a b'
@. Integer -> a
sel
  where
    as' :: Enumeration a
as' = [a] -> Enumeration a
forall a. [a] -> Enumeration a
E.finiteList [a]
as
    Finite Integer
n = Enumeration a -> Cardinality
forall a. Enumeration a -> Cardinality
E.card Enumeration a
as'
    sel :: Integer -> a
sel = Enumeration a -> Integer -> a
forall a. Enumeration a -> Integer -> a
E.select Enumeration a
as'

-- | @nat = 'mkProEnumeration' C.'C.nat' E.'E.nat'@
nat :: ProEnumeration Integer Integer
nat :: ProEnumeration Integer Integer
nat = CoEnumeration Integer
-> Enumeration Integer -> ProEnumeration Integer Integer
forall a b. CoEnumeration a -> Enumeration b -> ProEnumeration a b
mkProEnumeration CoEnumeration Integer
C.nat Enumeration Integer
E.nat

-- | @int = 'mkProEnumeration' C.'C.int' E.'E.int'@
int :: ProEnumeration Integer Integer
int :: ProEnumeration Integer Integer
int = CoEnumeration Integer
-> Enumeration Integer -> ProEnumeration Integer Integer
forall a b. CoEnumeration a -> Enumeration b -> ProEnumeration a b
mkProEnumeration CoEnumeration Integer
C.int Enumeration Integer
E.int

-- | @cw = 'mkProEnumeration' C.'C.cw' E.'E.cw'@
cw :: ProEnumeration Rational Rational
cw :: ProEnumeration Rational Rational
cw = CoEnumeration Rational
-> Enumeration Rational -> ProEnumeration Rational Rational
forall a b. CoEnumeration a -> Enumeration b -> ProEnumeration a b
mkProEnumeration CoEnumeration Rational
C.cw Enumeration Rational
E.cw

-- | @rat = 'mkProEnumeration' C.'C.rat' E.'E.rat'@
rat :: ProEnumeration Rational Rational
rat :: ProEnumeration Rational Rational
rat = CoEnumeration Rational
-> Enumeration Rational -> ProEnumeration Rational Rational
forall a b. CoEnumeration a -> Enumeration b -> ProEnumeration a b
mkProEnumeration CoEnumeration Rational
C.rat Enumeration Rational
E.rat

-- | Sets the cardinality of given proenumeration to 'Infinite'
infinite :: ProEnumeration a b -> ProEnumeration a b
infinite :: forall a b. ProEnumeration a b -> ProEnumeration a b
infinite ProEnumeration a b
p = ProEnumeration a b
p{ card = Infinite }

-- * Proenumeration combinators

-- | From two proenumerations @p, q@, we can make a proenumeration
--   @compose p q@ which behaves as a composed function
--   (in diagrammatic order like 'Control.Category.>>>'.)
--
--   > run (compose p q) = run q . run p
--
--   @p@ and @q@ can be drawn in a diagram as follows:
--
--   > [_______p______] [______q______]
--   >
--   >    lp      sp      lq      sq
--   > a ----> N ----> b ----> M ----> c
--
--   To get a proenumeration @a -> ?? -> c@, there are two obvious choices:
--
--   >       run p >>> lq         sq
--   > a --------------------> M ----> c
--   >    lp         sp >>> run q
--   > a ----> N --------------------> c
--
--   This function chooses the option with the smaller cardinality.
compose :: ProEnumeration a b -> ProEnumeration b c -> ProEnumeration a c
compose :: forall a b c.
ProEnumeration a b -> ProEnumeration b c -> ProEnumeration a c
compose ProEnumeration a b
p ProEnumeration b c
q
  | ProEnumeration a b -> Cardinality
forall a b. ProEnumeration a b -> Cardinality
card ProEnumeration a b
p Cardinality -> Cardinality -> Bool
forall a. Ord a => a -> a -> Bool
<= ProEnumeration b c -> Cardinality
forall a b. ProEnumeration a b -> Cardinality
card ProEnumeration b c
q = ProEnumeration a b
p ProEnumeration a b -> (b -> c) -> ProEnumeration a c
forall a b b'.
ProEnumeration a b -> (b -> b') -> ProEnumeration a b'
@. ProEnumeration b c -> b -> c
forall a b. ProEnumeration a b -> a -> b
run ProEnumeration b c
q
  | Bool
otherwise        = ProEnumeration a b -> a -> b
forall a b. ProEnumeration a b -> a -> b
run ProEnumeration a b
p (a -> b) -> ProEnumeration b c -> ProEnumeration a c
forall a' a b.
(a' -> a) -> ProEnumeration a b -> ProEnumeration a' b
.@ ProEnumeration b c
q

-- | Cartesian product of proenumerations.
--
-- @
-- p >< q = 'mkProEnumeration' (baseCoEnum p C.'C.><' baseCoEnum q)
--                             (baseEnum p   E.'E.><' baseEnum q)
-- @
--
-- This operation is not associative if and only if one of the arguments
-- is not finite.
(><) :: ProEnumeration a1 b1 -> ProEnumeration a2 b2 -> ProEnumeration (a1,a2) (b1,b2)
ProEnumeration a1 b1
p >< :: forall a1 b1 a2 b2.
ProEnumeration a1 b1
-> ProEnumeration a2 b2 -> ProEnumeration (a1, a2) (b1, b2)
>< ProEnumeration a2 b2
q = CoEnumeration (a1, a2)
-> Enumeration (b1, b2) -> ProEnumeration (a1, a2) (b1, b2)
forall a b. CoEnumeration a -> Enumeration b -> ProEnumeration a b
mkProEnumeration (ProEnumeration a1 b1 -> CoEnumeration a1
forall a b. ProEnumeration a b -> CoEnumeration a
baseCoEnum ProEnumeration a1 b1
p CoEnumeration a1 -> CoEnumeration a2 -> CoEnumeration (a1, a2)
forall a b.
CoEnumeration a -> CoEnumeration b -> CoEnumeration (a, b)
C.>< ProEnumeration a2 b2 -> CoEnumeration a2
forall a b. ProEnumeration a b -> CoEnumeration a
baseCoEnum ProEnumeration a2 b2
q) (ProEnumeration a1 b1 -> Enumeration b1
forall a b. ProEnumeration a b -> Enumeration b
baseEnum ProEnumeration a1 b1
p Enumeration b1 -> Enumeration b2 -> Enumeration (b1, b2)
forall a b. Enumeration a -> Enumeration b -> Enumeration (a, b)
E.>< ProEnumeration a2 b2 -> Enumeration b2
forall a b. ProEnumeration a b -> Enumeration b
baseEnum ProEnumeration a2 b2
q)

-- | Disjoint sum of proenumerations.
--
-- @
-- p <+> q = 'mkProEnumeration'
--    (baseCoEnum p C.'C.<+>'        baseCoEnum q)
--    (baseEnum p   `E.'E.eitherOf'` baseEnum q)
-- @
-- This operation is not associative if and only if one of the arguments
-- is not finite.
(<+>) :: ProEnumeration a1 b1 -> ProEnumeration a2 b2
      -> ProEnumeration (Either a1 a2) (Either b1 b2)
ProEnumeration a1 b1
p <+> :: forall a1 b1 a2 b2.
ProEnumeration a1 b1
-> ProEnumeration a2 b2
-> ProEnumeration (Either a1 a2) (Either b1 b2)
<+> ProEnumeration a2 b2
q = CoEnumeration (Either a1 a2)
-> Enumeration (Either b1 b2)
-> ProEnumeration (Either a1 a2) (Either b1 b2)
forall a b. CoEnumeration a -> Enumeration b -> ProEnumeration a b
mkProEnumeration (ProEnumeration a1 b1 -> CoEnumeration a1
forall a b. ProEnumeration a b -> CoEnumeration a
baseCoEnum ProEnumeration a1 b1
p CoEnumeration a1
-> CoEnumeration a2 -> CoEnumeration (Either a1 a2)
forall a b.
CoEnumeration a -> CoEnumeration b -> CoEnumeration (Either a b)
C.<+> ProEnumeration a2 b2 -> CoEnumeration a2
forall a b. ProEnumeration a b -> CoEnumeration a
baseCoEnum ProEnumeration a2 b2
q) (Enumeration b1 -> Enumeration b2 -> Enumeration (Either b1 b2)
forall a b.
Enumeration a -> Enumeration b -> Enumeration (Either a b)
E.eitherOf (ProEnumeration a1 b1 -> Enumeration b1
forall a b. ProEnumeration a b -> Enumeration b
baseEnum ProEnumeration a1 b1
p) (ProEnumeration a2 b2 -> Enumeration b2
forall a b. ProEnumeration a b -> Enumeration b
baseEnum ProEnumeration a2 b2
q))

-- | @maybeOf p = 'mkProEnumeration' (C.'C.maybeOf' (baseCoEnum p)) (E.'E.maybeOf' (baseEnum p))@
maybeOf :: ProEnumeration a b -> ProEnumeration (Maybe a) (Maybe b)
maybeOf :: forall a b.
ProEnumeration a b -> ProEnumeration (Maybe a) (Maybe b)
maybeOf ProEnumeration a b
p = (Maybe a -> Either () a)
-> (Either () b -> Maybe b)
-> ProEnumeration (Either () a) (Either () b)
-> ProEnumeration (Maybe a) (Maybe b)
forall a' a b b'.
(a' -> a)
-> (b -> b') -> ProEnumeration a b -> ProEnumeration a' b'
dimap (Either () a -> (a -> Either () a) -> Maybe a -> Either () a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> Either () a
forall a b. a -> Either a b
Left ()) a -> Either () a
forall a b. b -> Either a b
Right) ((() -> Maybe b) -> (b -> Maybe b) -> Either () b -> Maybe b
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe b -> () -> Maybe b
forall a b. a -> b -> a
const Maybe b
forall a. Maybe a
Nothing) b -> Maybe b
forall a. a -> Maybe a
Just) (ProEnumeration (Either () a) (Either () b)
 -> ProEnumeration (Maybe a) (Maybe b))
-> ProEnumeration (Either () a) (Either () b)
-> ProEnumeration (Maybe a) (Maybe b)
forall a b. (a -> b) -> a -> b
$
              ProEnumeration () ()
forall a. ProEnumeration a ()
unit ProEnumeration () ()
-> ProEnumeration a b -> ProEnumeration (Either () a) (Either () b)
forall a1 b1 a2 b2.
ProEnumeration a1 b1
-> ProEnumeration a2 b2
-> ProEnumeration (Either a1 a2) (Either b1 b2)
<+> ProEnumeration a b
p

-- | Synonym of '(<+>)'
eitherOf :: ProEnumeration a1 b1 -> ProEnumeration a2 b2
         -> ProEnumeration (Either a1 a2) (Either b1 b2)
eitherOf :: forall a1 b1 a2 b2.
ProEnumeration a1 b1
-> ProEnumeration a2 b2
-> ProEnumeration (Either a1 a2) (Either b1 b2)
eitherOf = ProEnumeration a1 b1
-> ProEnumeration a2 b2
-> ProEnumeration (Either a1 a2) (Either b1 b2)
forall a1 b1 a2 b2.
ProEnumeration a1 b1
-> ProEnumeration a2 b2
-> ProEnumeration (Either a1 a2) (Either b1 b2)
(<+>)

-- | @listOf p = 'mkProEnumeration' (C.'C.listOf' (baseCoEnum p)) (E.'E.listOf' (baseEnum p))@
listOf :: ProEnumeration a b -> ProEnumeration [a] [b]
listOf :: forall a b. ProEnumeration a b -> ProEnumeration [a] [b]
listOf ProEnumeration a b
p = CoEnumeration [a] -> Enumeration [b] -> ProEnumeration [a] [b]
forall a b. CoEnumeration a -> Enumeration b -> ProEnumeration a b
mkProEnumeration (CoEnumeration a -> CoEnumeration [a]
forall a. CoEnumeration a -> CoEnumeration [a]
C.listOf (ProEnumeration a b -> CoEnumeration a
forall a b. ProEnumeration a b -> CoEnumeration a
baseCoEnum ProEnumeration a b
p)) (Enumeration b -> Enumeration [b]
forall a. Enumeration a -> Enumeration [a]
E.listOf (ProEnumeration a b -> Enumeration b
forall a b. ProEnumeration a b -> Enumeration b
baseEnum ProEnumeration a b
p))

-- |
-- @
-- finiteSubsetOf p = 'mkProEnumeration'
--     (C.'C.finiteSubsetOf' (baseCoEnum p))
--     (E.'E.finiteSubsetOf' (baseEnum p))
-- @
finiteSubsetOf :: ProEnumeration a b -> ProEnumeration [a] [b]
finiteSubsetOf :: forall a b. ProEnumeration a b -> ProEnumeration [a] [b]
finiteSubsetOf ProEnumeration a b
p =
  CoEnumeration [a] -> Enumeration [b] -> ProEnumeration [a] [b]
forall a b. CoEnumeration a -> Enumeration b -> ProEnumeration a b
mkProEnumeration (CoEnumeration a -> CoEnumeration [a]
forall a. CoEnumeration a -> CoEnumeration [a]
C.finiteSubsetOf (ProEnumeration a b -> CoEnumeration a
forall a b. ProEnumeration a b -> CoEnumeration a
baseCoEnum ProEnumeration a b
p)) (Enumeration b -> Enumeration [b]
forall a. Enumeration a -> Enumeration [a]
E.finiteSubsetOf (ProEnumeration a b -> Enumeration b
forall a b. ProEnumeration a b -> Enumeration b
baseEnum ProEnumeration a b
p))

-- | Enumerate every possible proenumeration.
--
-- @enumerateP a b@ generates proenumerations @p@
-- such that the function @run p@ has the following properties:
--
-- * The range of @run p@ is a subset of @b :: Enumeration b@.
-- * If @locate a x = locate a y@, then @run p x = run p y@.
--   In other words, @run p@ factors through @locate a@.
--
-- This function generates proenumerations @p@ in such a way that
-- every function of type @a -> b@ with the above properties uniquely
-- appears as @run p@ for some enumerated @p@.
enumerateP :: CoEnumeration a -> Enumeration b -> Enumeration (ProEnumeration a b)
enumerateP :: forall a b.
CoEnumeration a
-> Enumeration b -> Enumeration (ProEnumeration a b)
enumerateP CoEnumeration a
a Enumeration b
b = case (CoEnumeration a -> Cardinality
forall a. CoEnumeration a -> Cardinality
C.card CoEnumeration a
a, Enumeration b -> Cardinality
forall a. Enumeration a -> Cardinality
E.card Enumeration b
b) of
  (Cardinality
0, Cardinality
_) -> ProEnumeration a b -> Enumeration (ProEnumeration a b)
forall a. a -> Enumeration a
E.singleton (CoEnumeration a -> Enumeration b -> ProEnumeration a b
forall a b. CoEnumeration a -> Enumeration b -> ProEnumeration a b
mkProEnumeration CoEnumeration a
a Enumeration b
forall a. Enumeration a
forall (f :: * -> *) a. Alternative f => f a
Ap.empty)
  (Cardinality
_, Cardinality
1) -> ProEnumeration a b -> Enumeration (ProEnumeration a b)
forall a. a -> Enumeration a
E.singleton (CoEnumeration a -> Enumeration b -> ProEnumeration a b
forall a b. CoEnumeration a -> Enumeration b -> ProEnumeration a b
mkProEnumeration CoEnumeration a
forall a. CoEnumeration a
C.unit Enumeration b
b)
  (Finite Integer
k,Cardinality
_) -> CoEnumeration a -> Enumeration b -> ProEnumeration a b
forall a b. CoEnumeration a -> Enumeration b -> ProEnumeration a b
mkProEnumeration CoEnumeration a
a (Enumeration b -> ProEnumeration a b)
-> Enumeration (Enumeration b) -> Enumeration (ProEnumeration a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Enumeration b -> Enumeration (Enumeration b)
forall a. Int -> Enumeration a -> Enumeration (Enumeration a)
E.finiteEnumerationOf (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
k) Enumeration b
b
  (Cardinality
Infinite,Cardinality
_) -> [Char] -> Enumeration (ProEnumeration a b)
forall a. HasCallStack => [Char] -> a
error [Char]
"infinite domain"

-- | Coenumerate every possible function.
--
-- @coenumerateP as bs@ classifies functions of type @a -> b@
-- by the following criterion:
--
-- @f@ and @g@ have the same index
--
-- /if and only if/
--
-- For all elements @a@ of @as :: Enumeration a@,
--   @locate bs (f a) = locate bs (g a)@.
--
-- /Note/: The suffix @P@ suggests it coenumerates @ProEnumeration a b@,
-- but it actually coenumerates @a -> b@.  The reason is that
-- @ProEnumeration a b@ carries extra data and constraints like its cardinality,
-- but the classification does not care about those. Thus, it is more permissive to
-- accept any function of type @a -> b@.
--
-- To force it to coenumerate proenumerations,
-- @'contramap' 'run'@ can be applied.
coenumerateP :: Enumeration a -> CoEnumeration b -> CoEnumeration (a -> b)
coenumerateP :: forall a b.
Enumeration a -> CoEnumeration b -> CoEnumeration (a -> b)
coenumerateP Enumeration a
a CoEnumeration b
b = case (Enumeration a -> Cardinality
forall a. Enumeration a -> Cardinality
E.card Enumeration a
a, CoEnumeration b -> Cardinality
forall a. CoEnumeration a -> Cardinality
C.card CoEnumeration b
b) of
  (Cardinality
0, Cardinality
_)       -> CoEnumeration (a -> b)
forall a. CoEnumeration a
C.unit
  (Cardinality
_, Cardinality
1)       -> CoEnumeration (a -> b)
forall a. CoEnumeration a
C.unit
  (Finite Integer
k,Cardinality
_) -> ((a -> b) -> Integer -> b)
-> CoEnumeration (Integer -> b) -> CoEnumeration (a -> b)
forall a' a. (a' -> a) -> CoEnumeration a -> CoEnumeration a'
forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap (\a -> b
f -> a -> b
f (a -> b) -> (Integer -> a) -> Integer -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Enumeration a -> Integer -> a
forall a. Enumeration a -> Integer -> a
E.select Enumeration a
a) (CoEnumeration (Integer -> b) -> CoEnumeration (a -> b))
-> CoEnumeration (Integer -> b) -> CoEnumeration (a -> b)
forall a b. (a -> b) -> a -> b
$ Integer -> CoEnumeration b -> CoEnumeration (Integer -> b)
forall a.
Integer -> CoEnumeration a -> CoEnumeration (Integer -> a)
C.finiteFunctionOf Integer
k CoEnumeration b
b
  (Cardinality
Infinite,Cardinality
_) -> [Char] -> CoEnumeration (a -> b)
forall a. HasCallStack => [Char] -> a
error [Char]
"infinite domain"

{- | 'enumerateP' and 'coenumerateP' combined.

>    l_a      s_a
> a -----> N -----> a'  :: ProEnumeration a a'
>
>    l_b      s_b
> b -----> M -----> b'  :: ProEnumeration b b'
>
>
> (N -> b) ---> (N -> M) ---> (N -> b')
>    ^             ||             |
>    | (. s_a)     ||             | (. l_a)
>    |             ||             v
> (a' -> b)      (M ^ N)       (a -> b')

* When @N@ is finite, @(M ^ N)@ is at most countable, since @M@ is
  at most countable.

* The enumerated functions (of type @a -> b'@) are compositions
  of @l_a :: a -> N@ and functions of type @N -> b@.
  It is beneficial to tell this fact by the type,
  which happens to be @ProEnumeration a b'@.

-}
proenumerationOf
  :: ProEnumeration a a'
  -> ProEnumeration b b'
  -> ProEnumeration (a' -> b) (ProEnumeration a b')
proenumerationOf :: forall a a' b b'.
ProEnumeration a a'
-> ProEnumeration b b'
-> ProEnumeration (a' -> b) (ProEnumeration a b')
proenumerationOf ProEnumeration a a'
a ProEnumeration b b'
b
  = CoEnumeration (a' -> b)
-> Enumeration (ProEnumeration a b')
-> ProEnumeration (a' -> b) (ProEnumeration a b')
forall a b. CoEnumeration a -> Enumeration b -> ProEnumeration a b
mkProEnumeration
      (Enumeration a' -> CoEnumeration b -> CoEnumeration (a' -> b)
forall a b.
Enumeration a -> CoEnumeration b -> CoEnumeration (a -> b)
coenumerateP (ProEnumeration a a' -> Enumeration a'
forall a b. ProEnumeration a b -> Enumeration b
baseEnum ProEnumeration a a'
a) (ProEnumeration b b' -> CoEnumeration b
forall a b. ProEnumeration a b -> CoEnumeration a
baseCoEnum ProEnumeration b b'
b))
      (CoEnumeration a
-> Enumeration b' -> Enumeration (ProEnumeration a b')
forall a b.
CoEnumeration a
-> Enumeration b -> Enumeration (ProEnumeration a b)
enumerateP (ProEnumeration a a' -> CoEnumeration a
forall a b. ProEnumeration a b -> CoEnumeration a
baseCoEnum ProEnumeration a a'
a) (ProEnumeration b b' -> Enumeration b'
forall a b. ProEnumeration a b -> Enumeration b
baseEnum ProEnumeration b b'
b))

-- | @finiteFunctionOf k p@ is a proenumeration of products of @k@ copies of
--   @a@ and @b@ respectively.
--
--   If @p@ is a invertible enumeration, @finiteFunctionOf k p@ is too.
--
--   It is implemented using 'proenumerationOf'.
finiteFunctionOf
  :: Integer -> ProEnumeration a b -> ProEnumeration (Integer -> a) (Integer -> b)
finiteFunctionOf :: forall a b.
Integer
-> ProEnumeration a b
-> ProEnumeration (Integer -> a) (Integer -> b)
finiteFunctionOf Integer
k ProEnumeration a b
p = ProEnumeration Integer Integer
-> ProEnumeration a b
-> ProEnumeration (Integer -> a) (ProEnumeration Integer b)
forall a a' b b'.
ProEnumeration a a'
-> ProEnumeration b b'
-> ProEnumeration (a' -> b) (ProEnumeration a b')
proenumerationOf (Integer -> ProEnumeration Integer Integer
modulo Integer
k) ProEnumeration a b
p ProEnumeration (Integer -> a) (ProEnumeration Integer b)
-> (ProEnumeration Integer b -> Integer -> b)
-> ProEnumeration (Integer -> a) (Integer -> b)
forall a b b'.
ProEnumeration a b -> (b -> b') -> ProEnumeration a b'
@. ProEnumeration Integer b -> Integer -> b
forall a b. ProEnumeration a b -> Integer -> b
select