-- |
-- Module      : Test.LeanCheck.Utils.TypeBinding
-- Copyright   : (c) 2015-2024 Rudy Matela
-- License     : 3-Clause BSD  (see the file LICENSE)
-- Maintainer  : Rudy Matela <rudy@matela.com.br>
--
-- This module is part of LeanCheck,
-- a simple enumerative property-based testing library.
--
-- Infix operators for type binding using dummy first-class values.
--
-- Those are useful when property based testing to avoid repetition.
-- Suppose:
--
-- > prop_sortAppend :: Ord a => [a] -> Bool
-- > prop_sortAppend xs =  sort (xs++ys) == sort (ys++xs)
--
-- Then this:
--
-- > testResults n =
-- >   [ holds n (prop_sortAppend :: [Int] -> [Int] -> Bool)
-- >   , holds n (prop_sortAppend :: [UInt2] -> [UInt2] -> Bool)
-- >   , holds n (prop_sortAppend :: [Bool] -> [Bool] -> Bool)
-- >   , holds n (prop_sortAppend :: [Char] -> [Char] -> Bool)
-- >   , holds n (prop_sortAppend :: [String] -> [String] -> Bool)
-- >   , holds n (prop_sortAppend :: [()] -> [()] -> Bool)
-- >   ]
--
-- Becomes this:
--
-- > testResults n =
-- >   [ holds n $ prop_sortAppend -:> [int]
-- >   , holds n $ prop_sortAppend -:> [uint2]
-- >   , holds n $ prop_sortAppend -:> [bool]
-- >   , holds n $ prop_sortAppend -:> [char]
-- >   , holds n $ prop_sortAppend -:> [string]
-- >   , holds n $ prop_sortAppend -:> [()]
-- >   ]
--
-- Or even:
--
-- > testResults n  =  concat
-- >   [ for int, for uint2, for bool, for (), for char, for string ]
-- >   where  for a  =  [ holds n $ prop_sortAppend -:> a ]
--
-- This last form is useful when testing multiple properties for multiple
-- types.
module Test.LeanCheck.Utils.TypeBinding
  (
  -- * Type binding operators
  --
  -- | Summary:
  --
  -- *                 as type of: '-:'
  -- *        argument as type of: '-:>'
  -- *          result as type of: '->:'
  -- * second argument as type of: '->:>'
  -- * second  result  as type of: '->>:'
  -- * third  argument as type of: '->>:>'
  -- * third   result  as type of: '->>>:'
    (-:)
  , (-:>)
  , (->:)
  , (->:>)
  , (->>:)
  , (->>:>)
  , (->>>:)
  , (->>>:>)
  , (->>>>:)
  , (->>>>:>)
  , (->>>>>:)
  , (->>>>>:>)
  , (->>>>>>:)
  , (->>>>>>:>)
  , (->>>>>>>:)
  , (->>>>>>>:>)
  , (->>>>>>>>:)
  , (->>>>>>>>:>)
  , (->>>>>>>>>:)
  , (->>>>>>>>>:>)
  , (->>>>>>>>>>:)
  , (->>>>>>>>>>:>)
  , (->>>>>>>>>>>:)
  , (->>>>>>>>>>>:>)
  , (->>>>>>>>>>>>:)

  -- * Dummy (undefined) values
  -- ** Standard Haskell types
  , und
  , (>-)
  , bool
  , int, integer
  , float, double
  , rational
  , char, string
  , ordering
  , mayb, eith
  -- ** Testing types
  , natural
  , nat
  , int1
  , int2
  , int3
  , int4
  , word1
  , word2
  , word3
  , word4
  -- *** Deprecated testing types
  , uint1
  , uint2
  , uint3
  , uint4
  )
where

import Test.LeanCheck.Utils.Types

undefinedOf :: String -> a
undefinedOf :: forall a. String -> a
undefinedOf String
fn  =  String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"Test.LeanCheck.Utils.undefinedOf " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fn

-- | Type restricted version of const
-- that forces its first argument
-- to have the same type as the second.
-- A symnonym to 'asTypeOf':
--
-- >  value -: ty  =  value :: Ty
--
-- Examples:
--
-- >  10 -: int   =  10 :: Int
-- >  undefined -: 'a' >- 'b'  =  undefined :: Char -> Char
(-:) :: a -> a -> a
-: :: forall a. a -> a -> a
(-:)  =  a -> a -> a
forall a. a -> a -> a
asTypeOf  -- const
infixl 1 -:

-- | Type restricted version of const
-- that forces the argument of its first argument
-- to have the same type as the second:
--
-- >  f -:> ty  =  f -: ty >- und  =  f :: Ty -> a
--
-- Example:
--
-- >  abs -:> int   =  abs -: int >- und  =  abs :: Int -> Int
(-:>) :: (a -> b) -> a -> (a -> b)
-:> :: forall a b. (a -> b) -> a -> a -> b
(-:>)  =  (a -> b) -> a -> a -> b
forall a b. a -> b -> a
const
infixl 1 -:>

-- | Type restricted version of const
-- that forces the result of its first argument
-- to have the same type as the second.
--
-- >  f ->: ty  =  f -: und >- ty  =  f :: a -> Ty
(->:) :: (a -> b) -> b -> (a -> b)
->: :: forall a b. (a -> b) -> b -> a -> b
(->:)  =  (a -> b) -> b -> a -> b
forall a b. a -> b -> a
const
infixl 1 ->:

-- | Type restricted version of const
-- that forces the second argument of its first argument
-- to have the same type as the second.
--
-- > f ->:> ty   =  f -: und -> ty -> und  =  f :: a -> Ty -> b
(->:>) :: (a -> b -> c) -> b -> (a -> b -> c)
->:> :: forall a b c. (a -> b -> c) -> b -> a -> b -> c
(->:>)  =  (a -> b -> c) -> b -> a -> b -> c
forall a b. a -> b -> a
const
infixl 1 ->:>

-- | Type restricted version of const
-- that forces the result of the result of its first argument
-- to have the same type as the second.
--
-- > f ->>: ty   =  f -: und -> und -> ty  =  f :: a -> b -> Ty
(->>:) :: (a -> b -> c) -> c -> (a -> b -> c)
->>: :: forall a b c. (a -> b -> c) -> c -> a -> b -> c
(->>:)  =  (a -> b -> c) -> c -> a -> b -> c
forall a b. a -> b -> a
const
infixl 1 ->>:

-- | Type restricted version of const
-- that forces the third argument of its first argument
-- to have the same type as the second.
(->>:>) :: (a -> b -> c -> d) -> c -> (a -> b -> c -> d)
->>:> :: forall a b c d. (a -> b -> c -> d) -> c -> a -> b -> c -> d
(->>:>)  =  (a -> b -> c -> d) -> c -> a -> b -> c -> d
forall a b. a -> b -> a
const
infixl 1 ->>:>

-- | Type restricted version of const
-- that forces the result of the result of the result of its first argument
-- to have the same type as the second.
(->>>:) :: (a -> b -> c -> d) -> d -> (a -> b -> c -> d)
->>>: :: forall a b c d. (a -> b -> c -> d) -> d -> a -> b -> c -> d
(->>>:)  =  (a -> b -> c -> d) -> d -> a -> b -> c -> d
forall a b. a -> b -> a
const
infixl 1 ->>>:

-- | Forces the 4th argument type.
(->>>:>) :: (a -> b -> c -> d -> e) -> d -> (a -> b -> c -> d -> e)
->>>:> :: forall a b c d e.
(a -> b -> c -> d -> e) -> d -> a -> b -> c -> d -> e
(->>>:>)  =  (a -> b -> c -> d -> e) -> d -> a -> b -> c -> d -> e
forall a b. a -> b -> a
const
infixl 1 ->>>:>

-- | Forces the result type of a 4-argument function.
(->>>>:) :: (a -> b -> c -> d -> e) -> e -> (a -> b -> c -> d -> e)
->>>>: :: forall a b c d e.
(a -> b -> c -> d -> e) -> e -> a -> b -> c -> d -> e
(->>>>:)  =  (a -> b -> c -> d -> e) -> e -> a -> b -> c -> d -> e
forall a b. a -> b -> a
const
infixl 1 ->>>>:

-- | Forces the 5th argument type.
(->>>>:>) :: (a -> b -> c -> d -> e -> f) -> e -> (a -> b -> c -> d -> e -> f)
->>>>:> :: forall a b c d e f.
(a -> b -> c -> d -> e -> f) -> e -> a -> b -> c -> d -> e -> f
(->>>>:>)  =  (a -> b -> c -> d -> e -> f) -> e -> a -> b -> c -> d -> e -> f
forall a b. a -> b -> a
const
infixl 1 ->>>>:>

-- | Forces the result type of a 5-argument function.
(->>>>>:) :: (a -> b -> c -> d -> e -> f) -> f -> (a -> b -> c -> d -> e -> f)
->>>>>: :: forall a b c d e f.
(a -> b -> c -> d -> e -> f) -> f -> a -> b -> c -> d -> e -> f
(->>>>>:)  =  (a -> b -> c -> d -> e -> f) -> f -> a -> b -> c -> d -> e -> f
forall a b. a -> b -> a
const
infixl 1 ->>>>>:

-- | Forces the 6th argument type.
(->>>>>:>) :: (a->b->c->d->e->f->g) -> f -> (a->b->c->d->e->f->g)
->>>>>:> :: forall a b c d e f g.
(a -> b -> c -> d -> e -> f -> g)
-> f -> a -> b -> c -> d -> e -> f -> g
(->>>>>:>)  =  (a -> b -> c -> d -> e -> f -> g)
-> f -> a -> b -> c -> d -> e -> f -> g
forall a b. a -> b -> a
const
infixl 1 ->>>>>:>

-- | Forces the result type of a 6-argument function.
(->>>>>>:) :: (a->b->c->d->e->f->g) -> g -> (a->b->c->d->e->f->g)
->>>>>>: :: forall a b c d e f g.
(a -> b -> c -> d -> e -> f -> g)
-> g -> a -> b -> c -> d -> e -> f -> g
(->>>>>>:)  =  (a -> b -> c -> d -> e -> f -> g)
-> g -> a -> b -> c -> d -> e -> f -> g
forall a b. a -> b -> a
const
infixl 1 ->>>>>>:

-- | Forces the 7th argument type.
(->>>>>>:>) :: (a->b->c->d->e->f->g->h) -> g -> (a->b->c->d->e->f->g->h)
->>>>>>:> :: forall a b c d e f g h.
(a -> b -> c -> d -> e -> f -> g -> h)
-> g -> a -> b -> c -> d -> e -> f -> g -> h
(->>>>>>:>)  =  (a -> b -> c -> d -> e -> f -> g -> h)
-> g -> a -> b -> c -> d -> e -> f -> g -> h
forall a b. a -> b -> a
const
infixl 1 ->>>>>>:>

-- | Forces the result type of a 7-argument function.
(->>>>>>>:) :: (a->b->c->d->e->f->g->h) -> h -> (a->b->c->d->e->f->g->h)
->>>>>>>: :: forall a b c d e f g h.
(a -> b -> c -> d -> e -> f -> g -> h)
-> h -> a -> b -> c -> d -> e -> f -> g -> h
(->>>>>>>:)  =  (a -> b -> c -> d -> e -> f -> g -> h)
-> h -> a -> b -> c -> d -> e -> f -> g -> h
forall a b. a -> b -> a
const
infixl 1 ->>>>>>>:

-- | Forces the 8th argument type.
(->>>>>>>:>) :: (a->b->c->d->e->f->g->h->i) -> h -> (a->b->c->d->e->f->g->h->i)
->>>>>>>:> :: forall a b c d e f g h i.
(a -> b -> c -> d -> e -> f -> g -> h -> i)
-> h -> a -> b -> c -> d -> e -> f -> g -> h -> i
(->>>>>>>:>)  =  (a -> b -> c -> d -> e -> f -> g -> h -> i)
-> h -> a -> b -> c -> d -> e -> f -> g -> h -> i
forall a b. a -> b -> a
const
infixl 1 ->>>>>>>:>

-- | Forces the result type of a 8-argument function.
(->>>>>>>>:) :: (a->b->c->d->e->f->g->h->i) -> i -> (a->b->c->d->e->f->g->h->i)
->>>>>>>>: :: forall a b c d e f g h i.
(a -> b -> c -> d -> e -> f -> g -> h -> i)
-> i -> a -> b -> c -> d -> e -> f -> g -> h -> i
(->>>>>>>>:)  =  (a -> b -> c -> d -> e -> f -> g -> h -> i)
-> i -> a -> b -> c -> d -> e -> f -> g -> h -> i
forall a b. a -> b -> a
const
infixl 1 ->>>>>>>>:

-- | Forces the 9th argument type.
(->>>>>>>>:>) :: (a->b->c->d->e->f->g->h->i->j) -> i
              -> (a->b->c->d->e->f->g->h->i->j)
->>>>>>>>:> :: forall a b c d e f g h i j.
(a -> b -> c -> d -> e -> f -> g -> h -> i -> j)
-> i -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j
(->>>>>>>>:>)  =  (a -> b -> c -> d -> e -> f -> g -> h -> i -> j)
-> i -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j
forall a b. a -> b -> a
const
infixl 1 ->>>>>>>>:>

-- | Forces the result type of a 9-argument function.
(->>>>>>>>>:) :: (a->b->c->d->e->f->g->h->i->j) -> j
              -> (a->b->c->d->e->f->g->h->i->j)
->>>>>>>>>: :: forall a b c d e f g h i j.
(a -> b -> c -> d -> e -> f -> g -> h -> i -> j)
-> j -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j
(->>>>>>>>>:)  =  (a -> b -> c -> d -> e -> f -> g -> h -> i -> j)
-> j -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j
forall a b. a -> b -> a
const
infixl 1 ->>>>>>>>>:

-- | Forces the type of the 10th argument.
(->>>>>>>>>:>) :: (a->b->c->d->e->f->g->h->i->j->k) -> j
               -> (a->b->c->d->e->f->g->h->i->j->k)
->>>>>>>>>:> :: forall a b c d e f g h i j k.
(a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k)
-> j -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k
(->>>>>>>>>:>)  =  (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k)
-> j -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k
forall a b. a -> b -> a
const
infixl 1 ->>>>>>>>>:>

-- | Forces the result type of a 10-argument function.
(->>>>>>>>>>:) :: (a->b->c->d->e->f->g->h->i->j->k) -> k
               -> (a->b->c->d->e->f->g->h->i->j->k)
->>>>>>>>>>: :: forall a b c d e f g h i j k.
(a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k)
-> k -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k
(->>>>>>>>>>:)  =  (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k)
-> k -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k
forall a b. a -> b -> a
const
infixl 1 ->>>>>>>>>>:

-- | Forces the type of the 11th argument.
(->>>>>>>>>>:>) :: (a->b->c->d->e->f->g->h->i->j->k->l) -> k
                -> (a->b->c->d->e->f->g->h->i->j->k->l)
->>>>>>>>>>:> :: forall a b c d e f g h i j k l.
(a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l)
-> k -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l
(->>>>>>>>>>:>)  =  (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l)
-> k -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l
forall a b. a -> b -> a
const
infixl 1 ->>>>>>>>>>:>

-- | Forces the result type of a 11-argument function.
(->>>>>>>>>>>:) :: (a->b->c->d->e->f->g->h->i->j->k->l) -> l
                -> (a->b->c->d->e->f->g->h->i->j->k->l)
->>>>>>>>>>>: :: forall a b c d e f g h i j k l.
(a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l)
-> l -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l
(->>>>>>>>>>>:)  =  (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l)
-> l -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l
forall a b. a -> b -> a
const
infixl 1 ->>>>>>>>>>>:

-- | Forces the type of the 12th argument.
(->>>>>>>>>>>:>) :: (a->b->c->d->e->f->g->h->i->j->k->l->m) -> m
                 -> (a->b->c->d->e->f->g->h->i->j->k->l->m)
->>>>>>>>>>>:> :: forall a b c d e f g h i j k l m.
(a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m)
-> m
-> a
-> b
-> c
-> d
-> e
-> f
-> g
-> h
-> i
-> j
-> k
-> l
-> m
(->>>>>>>>>>>:>)  =  (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m)
-> m
-> a
-> b
-> c
-> d
-> e
-> f
-> g
-> h
-> i
-> j
-> k
-> l
-> m
forall a b. a -> b -> a
const
infixl 1 ->>>>>>>>>>>:>

-- | Forces the result type of a 12-argument function.
(->>>>>>>>>>>>:) :: (a->b->c->d->e->f->g->h->i->j->k->l->m) -> m
                 -> (a->b->c->d->e->f->g->h->i->j->k->l->m)
->>>>>>>>>>>>: :: forall a b c d e f g h i j k l m.
(a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m)
-> m
-> a
-> b
-> c
-> d
-> e
-> f
-> g
-> h
-> i
-> j
-> k
-> l
-> m
(->>>>>>>>>>>>:)  =  (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m)
-> m
-> a
-> b
-> c
-> d
-> e
-> f
-> g
-> h
-> i
-> j
-> k
-> l
-> m
forall a b. a -> b -> a
const
infixl 1 ->>>>>>>>>>>>:

-- | Returns an undefined functional value
-- that takes an argument of the type of its first argument
-- and return a value of the type of its second argument.
--
-- > ty >- ty  =  (undefined :: Ty -> Ty)
--
-- Examples:
--
-- > 'a' >- 'b'  =  char >- char  =  (undefined :: Char -> Char)
-- > int >- bool >- int  =  undefined :: Int -> Bool -> Int
(>-) :: a -> b -> (a -> b)
>- :: forall a b. a -> b -> a -> b
(>-)  =  String -> a -> b -> a -> b
forall a. String -> a
undefinedOf String
"(>-): undefined function -- using dummy value?"
infixr 9 >-


-- Dummy values of standard Haskell types

-- | Shorthand for undefined
und :: a
und :: forall a. a
und  =  String -> a
forall a. String -> a
undefinedOf String
"und"

-- | Undefined 'Int' value for use with type binding operators.
--
-- > check $ (\x y -> x + y == y + x) ->:> int
int :: Int
int :: Int
int  =  String -> Int
forall a. String -> a
undefinedOf String
"int"

-- | Undefined 'Integer' value for use with type binding operators.
--
-- > check $ (\x y -> x + y == y + x) ->:> integer
integer :: Integer
integer :: Integer
integer  =  String -> Integer
forall a. String -> a
undefinedOf String
"integer"

-- | Undefined 'Float' value for use with type binding operators.
float :: Float
float :: Float
float  =  String -> Float
forall a. String -> a
undefinedOf String
"float"

-- | Undefined 'Double' value for use with type binding operators.
double :: Double
double :: Double
double  =  String -> Double
forall a. String -> a
undefinedOf String
"double"

-- | Undefined 'Rational' value for use with type binding operators.
rational :: Rational
rational :: Rational
rational  =  String -> Rational
forall a. String -> a
undefinedOf String
"rational"

-- | Undefined 'Bool' value.
bool :: Bool
bool :: Bool
bool  =  String -> Bool
forall a. String -> a
undefinedOf String
"bool"

-- | Undefined 'Char' value.
char :: Char
char :: Char
char  =  String -> Char
forall a. String -> a
undefinedOf String
"char"

-- | Undefined 'String' value.
string :: String
string :: String
string  =  String -> String
forall a. String -> a
undefinedOf String
"string"

-- | Undefined 'Ordering' value.
ordering :: Ordering
ordering :: Ordering
ordering  =  String -> Ordering
forall a. String -> a
undefinedOf String
"ordering"

-- | Undefined 'Maybe' value.  Uses the type of the given value as the argument
--   type.  For use with type binding operators.
--
-- To check a property with the first argument bound to 'Maybe' 'Int', do:
--
-- > check $ prop -:> mayb int
mayb :: a -> Maybe a
mayb :: forall a. a -> Maybe a
mayb  =  String -> a -> Maybe a
forall a. String -> a
undefinedOf String
"mayb"

-- | Undefined 'Either' value.  Uses the types of the given values as the
--   argument types.  For use with type binding operators.
eith :: a -> b -> Either a b
eith :: forall a b. a -> b -> Either a b
eith  =  String -> a -> b -> Either a b
forall a. String -> a
undefinedOf String
"eith"


-- Dummy values of Test.LeanCheck.Types's types:

-- | Undefined 'Natural' value.
natural :: Natural
natural :: Natural
natural  =  String -> Natural
forall a. String -> a
undefinedOf String
"natural"

-- | Undefined 'Nat' value.
nat :: Nat
nat :: Nat
nat  =  String -> Nat
forall a. String -> a
undefinedOf String
"nat"

-- | Undefined 'Int1' value.
int1 :: Int1
int1 :: Int1
int1  =  String -> Int1
forall a. String -> a
undefinedOf String
"int1"

-- | Undefined 'Int2' value.
int2 :: Int2
int2 :: Int2
int2  =  String -> Int2
forall a. String -> a
undefinedOf String
"int2"

-- | Undefined 'Int3' value.
int3 :: Int3
int3 :: Int3
int3  =  String -> Int3
forall a. String -> a
undefinedOf String
"int3"

-- | Undefined 'Int4' value.
int4 :: Int4
int4 :: Int4
int4  =  String -> Int4
forall a. String -> a
undefinedOf String
"int4"

-- | Undefined 'Word1' value.
word1 :: Word1
word1 :: Word1
word1  =  String -> Word1
forall a. String -> a
undefinedOf String
"word1"

-- | Undefined 'Word2' value.
word2 :: Word2
word2 :: Word2
word2  =  String -> Word2
forall a. String -> a
undefinedOf String
"word2"

-- | Undefined 'Word3' value.
word3 :: Word3
word3 :: Word3
word3  =  String -> Word3
forall a. String -> a
undefinedOf String
"word3"

-- | Undefined 'Word4' value.
word4 :: Word4
word4 :: Word4
word4  =  String -> Word4
forall a. String -> a
undefinedOf String
"word4"

-- | Deprecated.  Use 'word1'.
uint1 :: UInt1
uint1 :: Word1
uint1  =  String -> Word1
forall a. String -> a
undefinedOf String
"uint1"

-- | Deprecated.  Use 'word2'.
uint2 :: UInt2
uint2 :: Word2
uint2  =  String -> Word2
forall a. String -> a
undefinedOf String
"uint2"

-- | Deprecated.  Use 'word3'.
uint3 :: UInt3
uint3 :: Word3
uint3  =  String -> Word3
forall a. String -> a
undefinedOf String
"uint3"

-- | Deprecated.  Use 'word4'.
uint4 :: UInt4
uint4 :: Word4
uint4  =  String -> Word4
forall a. String -> a
undefinedOf String
"uint4"