-- |
-- Module      : Test.LeanCheck.Utils.TypeBinding
-- Copyright   : (c) 2015-2020 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 :: 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.TypeBinding." 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
-: :: 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)
-:> :: (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)
->: :: (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)
->:> :: (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)
->>: :: (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)
->>:> :: (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)
->>>: :: (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)
->>>:> :: (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)
->>>>: :: (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)
->>>>:> :: (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)
->>>>>: :: (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)
->>>>>:> :: (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)
->>>>>>: :: (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)
->>>>>>:> :: (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)
->>>>>>>: :: (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)
->>>>>>>:> :: (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)
->>>>>>>>: :: (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)
->>>>>>>>:> :: (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)
->>>>>>>>>: :: (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)
->>>>>>>>>:> :: (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)
->>>>>>>>>>: :: (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)
->>>>>>>>>>:> :: (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)
->>>>>>>>>>>: :: (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)
->>>>>>>>>>>:> :: (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)
->>>>>>>>>>>>: :: (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)
>- :: 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 :: 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 :: 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 :: 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"