{-# LANGUAGE CPP #-} -- for GHC <= 7.8
-- |
-- Module      : Test.Extrapolate.Generalizable
-- Copyright   : (c) 2017-2019 Rudy Matela
-- License     : 3-Clause BSD  (see the file LICENSE)
-- Maintainer  : Rudy Matela <rudy@matela.com.br>
--
-- This module is part of Extrapolate,
-- a library for generalization of counter-examples.
--
-- This defines the 'Generalizable' typeclass
-- and utilities involving it.
--
-- You are probably better off importing "Test.Extrapolate".
module Test.Extrapolate.Generalizable
  ( Generalizable (..)
  , instances

  , mkEq1
  , mkEq2
  , mkEq3
  , mkEq4
  , mkOrd1
  , mkOrd2
  , mkOrd3
  , mkOrd4

  , (*==*)
  , (*/=*)
  , (*<=*)
  , (*<*)

  , Listable (..)
  , module Test.Extrapolate.Expr
  )
where

import Data.Maybe
import Data.Ratio

import Test.LeanCheck
import Test.LeanCheck.Utils

import Test.Extrapolate.TypeBinding
import Test.Extrapolate.Utils
import Test.Extrapolate.Expr

-- |
-- Extrapolate can generalize counter-examples of any types that are
-- 'Generalizable'.
--
-- 'Generalizable' types must first be instances of
--
-- * 'Listable', so Extrapolate knows how to enumerate values;
-- * 'Express', so Extrapolate can represent then manipulate values;
-- * 'Name', so Extrapolate knows how to name variables.
--
-- There are no required functions, so we can define instances with:
--
-- > instance Generalizable OurType
--
-- However, it is desirable to define both 'background' and 'subInstances'.
--
-- The following example shows a datatype and its instance:
--
-- > data Stack a = Stack a (Stack a) | Empty
--
-- > instance Generalizable a => Generalizable (Stack a) where
-- >   subInstances s  =  instances (argTy1of1 s)
--
-- To declare 'instances' it may be useful to use type binding
-- operators such as: 'argTy1of1', 'argTy1of2' and 'argTy2of2'.
--
-- Instances can be automatically derived using
-- 'Test.Extrapolate.Derive.deriveGeneralizable'
-- which will also automatically derivate
-- 'Listable', 'Express' and 'Name' when needed.
class (Listable a, Express a, Name a, Show a) => Generalizable a where
  -- | List of symbols allowed to appear in side-conditions.
  --   Defaults to @[]@.  See 'value'.
  background :: a -> [Expr]
  background a
_  =  []

  -- | Computes a list of reified subtype instances.
  --   Defaults to 'id'.
  --   See 'instances'.
  subInstances :: a -> Instances -> Instances
  subInstances a
_  =  [Expr] -> [Expr]
forall a. a -> a
id


instance Generalizable ()

instance Generalizable Bool where
  background :: Bool -> [Expr]
background Bool
p  =  Bool -> [Expr]
forall a. (Typeable a, Eq a) => a -> [Expr]
reifyEq Bool
p
                [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [ String -> (Bool -> Bool) -> Expr
forall a. Typeable a => String -> a -> Expr
value String
"not" Bool -> Bool
not ]

instance Generalizable Int where
  background :: Int -> [Expr]
background Int
x  =  Int -> [Expr]
forall a. (Typeable a, Ord a) => a -> [Expr]
reifyEqOrd Int
x

instance Generalizable Integer where
  background :: Integer -> [Expr]
background Integer
x  =  Integer -> [Expr]
forall a. (Typeable a, Ord a) => a -> [Expr]
reifyEqOrd Integer
x

instance Generalizable Char where
  background :: Char -> [Expr]
background Char
c  =  Char -> [Expr]
forall a. (Typeable a, Ord a) => a -> [Expr]
reifyEqOrd Char
c

instance (Generalizable a) => Generalizable (Maybe a) where
  background :: Maybe a -> [Expr]
background Maybe a
mx  =  ((a -> a -> Bool) -> Maybe a -> Maybe a -> Bool) -> [Expr]
forall a b.
(Generalizable a, Generalizable b) =>
((b -> b -> Bool) -> a -> a -> Bool) -> [Expr]
mkEq1  ((a -> a -> Bool) -> Maybe a -> Maybe a -> Bool
forall a. (a -> a -> Bool) -> Maybe a -> Maybe a -> Bool
maybeEq  ((a -> a -> Bool) -> Maybe a -> Maybe a -> Bool)
-> Maybe a -> (a -> a -> Bool) -> Maybe a -> Maybe a -> Bool
forall a b c. (a -> b -> c) -> b -> a -> b -> c
->:> Maybe a
mx)
                 [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ ((a -> a -> Bool) -> Maybe a -> Maybe a -> Bool) -> [Expr]
forall a b.
(Generalizable a, Generalizable b) =>
((b -> b -> Bool) -> a -> a -> Bool) -> [Expr]
mkOrd1 ((a -> a -> Bool) -> Maybe a -> Maybe a -> Bool
forall a. (a -> a -> Bool) -> Maybe a -> Maybe a -> Bool
maybeOrd ((a -> a -> Bool) -> Maybe a -> Maybe a -> Bool)
-> Maybe a -> (a -> a -> Bool) -> Maybe a -> Maybe a -> Bool
forall a b c. (a -> b -> c) -> b -> a -> b -> c
->:> Maybe a
mx)
                 [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [ String -> (a -> Maybe a) -> Expr
forall a. Typeable a => String -> a -> Expr
value String
"Just" (a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> Maybe a -> a -> Maybe a
forall a b. (a -> b) -> b -> a -> b
->: Maybe a
mx) ]
  subInstances :: Maybe a -> [Expr] -> [Expr]
subInstances Maybe a
mx  =  a -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances (Maybe a -> a
forall a. HasCallStack => Maybe a -> a
fromJust Maybe a
mx)

-- TODO: move maybeEq and maybeOrd here, I'll have to change the tests

instance (Generalizable a, Generalizable b) => Generalizable (Either a b) where
  background :: Either a b -> [Expr]
background Either a b
exy  =  ((a -> a -> Bool)
 -> (b -> b -> Bool) -> Either a b -> Either a b -> Bool)
-> [Expr]
forall a b c.
(Generalizable a, Generalizable b, Generalizable c) =>
((b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool) -> [Expr]
mkEq2  ((a -> a -> Bool)
-> (b -> b -> Bool) -> Either a b -> Either a b -> Bool
forall a b.
(a -> a -> Bool)
-> (b -> b -> Bool) -> Either a b -> Either a b -> Bool
eitherEq  ((a -> a -> Bool)
 -> (b -> b -> Bool) -> Either a b -> Either a b -> Bool)
-> Either a b
-> (a -> a -> Bool)
-> (b -> b -> Bool)
-> Either a b
-> Either a b
-> Bool
forall a b c d. (a -> b -> c -> d) -> c -> a -> b -> c -> d
->>:> Either a b
exy)
                  [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ ((a -> a -> Bool)
 -> (b -> b -> Bool) -> Either a b -> Either a b -> Bool)
-> [Expr]
forall a b c.
(Generalizable a, Generalizable b, Generalizable c) =>
((b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool) -> [Expr]
mkOrd2 ((a -> a -> Bool)
-> (b -> b -> Bool) -> Either a b -> Either a b -> Bool
forall a b.
(a -> a -> Bool)
-> (b -> b -> Bool) -> Either a b -> Either a b -> Bool
eitherOrd ((a -> a -> Bool)
 -> (b -> b -> Bool) -> Either a b -> Either a b -> Bool)
-> Either a b
-> (a -> a -> Bool)
-> (b -> b -> Bool)
-> Either a b
-> Either a b
-> Bool
forall a b c d. (a -> b -> c -> d) -> c -> a -> b -> c -> d
->>:> Either a b
exy)
                  [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [ String -> (a -> Either a b) -> Expr
forall a. Typeable a => String -> a -> Expr
value String
"Left"  (a -> Either a b
forall a b. a -> Either a b
Left  (a -> Either a b) -> Either a b -> a -> Either a b
forall a b. (a -> b) -> b -> a -> b
->: Either a b
exy)
                     , String -> (b -> Either a b) -> Expr
forall a. Typeable a => String -> a -> Expr
value String
"Right" (b -> Either a b
forall a b. b -> Either a b
Right (b -> Either a b) -> Either a b -> b -> Either a b
forall a b. (a -> b) -> b -> a -> b
->: Either a b
exy) ]
  subInstances :: Either a b -> [Expr] -> [Expr]
subInstances Either a b
exy  =  a -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances (Either a b -> a
forall a b. Either a b -> a
fromLeft  Either a b
exy)
                    ([Expr] -> [Expr]) -> ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  b -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances (Either a b -> b
forall a b. Either a b -> b
fromRight Either a b
exy)

-- TODO: move eitherEq and eitherOrd here, I'll have to change the tests

instance (Generalizable a, Generalizable b) => Generalizable (a,b) where
  background :: (a, b) -> [Expr]
background (a, b)
xy  =  ((a -> a -> Bool) -> (b -> b -> Bool) -> (a, b) -> (a, b) -> Bool)
-> [Expr]
forall a b c.
(Generalizable a, Generalizable b, Generalizable c) =>
((b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool) -> [Expr]
mkEq2  ((a -> a -> Bool) -> (b -> b -> Bool) -> (a, b) -> (a, b) -> Bool
forall a b.
(a -> a -> Bool) -> (b -> b -> Bool) -> (a, b) -> (a, b) -> Bool
pairEq  ((a -> a -> Bool) -> (b -> b -> Bool) -> (a, b) -> (a, b) -> Bool)
-> (a, b)
-> (a -> a -> Bool)
-> (b -> b -> Bool)
-> (a, b)
-> (a, b)
-> Bool
forall a b c d. (a -> b -> c -> d) -> c -> a -> b -> c -> d
->>:> (a, b)
xy)
                 [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ ((a -> a -> Bool) -> (b -> b -> Bool) -> (a, b) -> (a, b) -> Bool)
-> [Expr]
forall a b c.
(Generalizable a, Generalizable b, Generalizable c) =>
((b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool) -> [Expr]
mkOrd2 ((a -> a -> Bool) -> (b -> b -> Bool) -> (a, b) -> (a, b) -> Bool
forall a b.
(a -> a -> Bool) -> (b -> b -> Bool) -> (a, b) -> (a, b) -> Bool
pairOrd ((a -> a -> Bool) -> (b -> b -> Bool) -> (a, b) -> (a, b) -> Bool)
-> (a, b)
-> (a -> a -> Bool)
-> (b -> b -> Bool)
-> (a, b)
-> (a, b)
-> Bool
forall a b c d. (a -> b -> c -> d) -> c -> a -> b -> c -> d
->>:> (a, b)
xy)
  subInstances :: (a, b) -> [Expr] -> [Expr]
subInstances (a, b)
xy  =  a -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances ((a, b) -> a
forall a b. (a, b) -> a
fst (a, b)
xy)
                   ([Expr] -> [Expr]) -> ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  b -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances ((a, b) -> b
forall a b. (a, b) -> b
snd (a, b)
xy)

instance (Generalizable a, Generalizable b, Generalizable c)
      => Generalizable (a,b,c) where
  background :: (a, b, c) -> [Expr]
background (a, b, c)
xyz  =  ((a -> a -> Bool)
 -> (b -> b -> Bool)
 -> (c -> c -> Bool)
 -> (a, b, c)
 -> (a, b, c)
 -> Bool)
-> [Expr]
forall a b c d.
(Generalizable a, Generalizable b, Generalizable c,
 Generalizable d) =>
((b -> b -> Bool)
 -> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool)
-> [Expr]
mkEq3  ((a -> a -> Bool)
-> (b -> b -> Bool)
-> (c -> c -> Bool)
-> (a, b, c)
-> (a, b, c)
-> Bool
forall a b c.
(a -> a -> Bool)
-> (b -> b -> Bool)
-> (c -> c -> Bool)
-> (a, b, c)
-> (a, b, c)
-> Bool
tripleEq  ((a -> a -> Bool)
 -> (b -> b -> Bool)
 -> (c -> c -> Bool)
 -> (a, b, c)
 -> (a, b, c)
 -> Bool)
-> (a, b, c)
-> (a -> a -> Bool)
-> (b -> b -> Bool)
-> (c -> c -> Bool)
-> (a, b, c)
-> (a, b, c)
-> Bool
forall a b c d e.
(a -> b -> c -> d -> e) -> d -> a -> b -> c -> d -> e
->>>:> (a, b, c)
xyz)
                  [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ ((a -> a -> Bool)
 -> (b -> b -> Bool)
 -> (c -> c -> Bool)
 -> (a, b, c)
 -> (a, b, c)
 -> Bool)
-> [Expr]
forall a b c d.
(Generalizable a, Generalizable b, Generalizable c,
 Generalizable d) =>
((b -> b -> Bool)
 -> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool)
-> [Expr]
mkOrd3 ((a -> a -> Bool)
-> (b -> b -> Bool)
-> (c -> c -> Bool)
-> (a, b, c)
-> (a, b, c)
-> Bool
forall a b c.
(a -> a -> Bool)
-> (b -> b -> Bool)
-> (c -> c -> Bool)
-> (a, b, c)
-> (a, b, c)
-> Bool
tripleOrd ((a -> a -> Bool)
 -> (b -> b -> Bool)
 -> (c -> c -> Bool)
 -> (a, b, c)
 -> (a, b, c)
 -> Bool)
-> (a, b, c)
-> (a -> a -> Bool)
-> (b -> b -> Bool)
-> (c -> c -> Bool)
-> (a, b, c)
-> (a, b, c)
-> Bool
forall a b c d e.
(a -> b -> c -> d -> e) -> d -> a -> b -> c -> d -> e
->>>:> (a, b, c)
xyz)
  subInstances :: (a, b, c) -> [Expr] -> [Expr]
subInstances (a, b, c)
xyz  =  a -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances a
x ([Expr] -> [Expr]) -> ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances b
y ([Expr] -> [Expr]) -> ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances c
z
                       where (a
x,b
y,c
z) = (a, b, c)
xyz

instance (Generalizable a, Generalizable b, Generalizable c, Generalizable d)
      => Generalizable (a,b,c,d) where
  background :: (a, b, c, d) -> [Expr]
background (a, b, c, d)
xyzw  =  ((a -> a -> Bool)
 -> (b -> b -> Bool)
 -> (c -> c -> Bool)
 -> (d -> d -> Bool)
 -> (a, b, c, d)
 -> (a, b, c, d)
 -> Bool)
-> [Expr]
forall a b c d e.
(Generalizable a, Generalizable b, Generalizable c,
 Generalizable d, Generalizable e) =>
((b -> b -> Bool)
 -> (c -> c -> Bool)
 -> (d -> d -> Bool)
 -> (e -> e -> Bool)
 -> a
 -> a
 -> Bool)
-> [Expr]
mkEq4  ((a -> a -> Bool)
-> (b -> b -> Bool)
-> (c -> c -> Bool)
-> (d -> d -> Bool)
-> (a, b, c, d)
-> (a, b, c, d)
-> Bool
forall a b c d.
(a -> a -> Bool)
-> (b -> b -> Bool)
-> (c -> c -> Bool)
-> (d -> d -> Bool)
-> (a, b, c, d)
-> (a, b, c, d)
-> Bool
quadrupleEq  ((a -> a -> Bool)
 -> (b -> b -> Bool)
 -> (c -> c -> Bool)
 -> (d -> d -> Bool)
 -> (a, b, c, d)
 -> (a, b, c, d)
 -> Bool)
-> (a, b, c, d)
-> (a -> a -> Bool)
-> (b -> b -> Bool)
-> (c -> c -> Bool)
-> (d -> d -> Bool)
-> (a, b, c, d)
-> (a, b, c, d)
-> Bool
forall a b c d e f.
(a -> b -> c -> d -> e -> f) -> e -> a -> b -> c -> d -> e -> f
->>>>:> (a, b, c, d)
xyzw)
                   [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ ((a -> a -> Bool)
 -> (b -> b -> Bool)
 -> (c -> c -> Bool)
 -> (d -> d -> Bool)
 -> (a, b, c, d)
 -> (a, b, c, d)
 -> Bool)
-> [Expr]
forall a b c d e.
(Generalizable a, Generalizable b, Generalizable c,
 Generalizable d, Generalizable e) =>
((b -> b -> Bool)
 -> (c -> c -> Bool)
 -> (d -> d -> Bool)
 -> (e -> e -> Bool)
 -> a
 -> a
 -> Bool)
-> [Expr]
mkOrd4 ((a -> a -> Bool)
-> (b -> b -> Bool)
-> (c -> c -> Bool)
-> (d -> d -> Bool)
-> (a, b, c, d)
-> (a, b, c, d)
-> Bool
forall a b c d.
(a -> a -> Bool)
-> (b -> b -> Bool)
-> (c -> c -> Bool)
-> (d -> d -> Bool)
-> (a, b, c, d)
-> (a, b, c, d)
-> Bool
quadrupleOrd ((a -> a -> Bool)
 -> (b -> b -> Bool)
 -> (c -> c -> Bool)
 -> (d -> d -> Bool)
 -> (a, b, c, d)
 -> (a, b, c, d)
 -> Bool)
-> (a, b, c, d)
-> (a -> a -> Bool)
-> (b -> b -> Bool)
-> (c -> c -> Bool)
-> (d -> d -> Bool)
-> (a, b, c, d)
-> (a, b, c, d)
-> Bool
forall a b c d e f.
(a -> b -> c -> d -> e -> f) -> e -> a -> b -> c -> d -> e -> f
->>>>:> (a, b, c, d)
xyzw)
  subInstances :: (a, b, c, d) -> [Expr] -> [Expr]
subInstances (a, b, c, d)
xyzw  =  a -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances a
x
                     ([Expr] -> [Expr]) -> ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  b -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances b
y
                     ([Expr] -> [Expr]) -> ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  c -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances c
z
                     ([Expr] -> [Expr]) -> ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  d -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances d
w
                     where (a
x,b
y,c
z,d
w) = (a, b, c, d)
xyzw

instance Generalizable a => Generalizable [a] where
  background :: [a] -> [Expr]
background [a]
xs  =  ((a -> a -> Bool) -> [a] -> [a] -> Bool) -> [Expr]
forall a b.
(Generalizable a, Generalizable b) =>
((b -> b -> Bool) -> a -> a -> Bool) -> [Expr]
mkEq1  ((a -> a -> Bool) -> [a] -> [a] -> Bool
forall a. (a -> a -> Bool) -> [a] -> [a] -> Bool
listEq  ((a -> a -> Bool) -> [a] -> [a] -> Bool)
-> [a] -> (a -> a -> Bool) -> [a] -> [a] -> Bool
forall a b c. (a -> b -> c) -> b -> a -> b -> c
->:> [a]
xs)
                 [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ ((a -> a -> Bool) -> [a] -> [a] -> Bool) -> [Expr]
forall a b.
(Generalizable a, Generalizable b) =>
((b -> b -> Bool) -> a -> a -> Bool) -> [Expr]
mkOrd1 ((a -> a -> Bool) -> [a] -> [a] -> Bool
forall a. (a -> a -> Bool) -> [a] -> [a] -> Bool
listOrd ((a -> a -> Bool) -> [a] -> [a] -> Bool)
-> [a] -> (a -> a -> Bool) -> [a] -> [a] -> Bool
forall a b c. (a -> b -> c) -> b -> a -> b -> c
->:> [a]
xs)
                 [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [ String -> ([a] -> Int) -> Expr
forall a. Typeable a => String -> a -> Expr
value String
"length" ([a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([a] -> Int) -> [a] -> [a] -> Int
forall a b. (a -> b) -> a -> a -> b
-:> [a]
xs) ]
                 [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [ String -> (a -> [a] -> Bool) -> Expr
forall a. Typeable a => String -> a -> Expr
value String
"elem"      ((a -> a -> Bool) -> a -> [a] -> Bool
forall a. (a -> a -> Bool) -> a -> [a] -> Bool
elemBy a -> a -> Bool
forall a. Generalizable a => a -> a -> Bool
(*==*) (a -> [a] -> Bool) -> [a] -> a -> [a] -> Bool
forall a b c. (a -> b -> c) -> b -> a -> b -> c
->:> [a]
xs) | a -> Bool
forall a. Generalizable a => a -> Bool
hasEq (a -> Bool) -> a -> Bool
forall a b. (a -> b) -> a -> b
$ [a] -> a
forall a. [a] -> a
head [a]
xs ]
  subInstances :: [a] -> [Expr] -> [Expr]
subInstances [a]
xs  =  a -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances ([a] -> a
forall a. [a] -> a
head [a]
xs)

instance Generalizable Ordering where
  background :: Ordering -> [Expr]
background Ordering
o  =  Ordering -> [Expr]
forall a. (Typeable a, Ord a) => a -> [Expr]
reifyEqOrd Ordering
o

mkEq1 :: (Generalizable a, Generalizable b)
      => ((b -> b -> Bool) -> a -> a -> Bool) -> [Expr]
mkEq1 :: ((b -> b -> Bool) -> a -> a -> Bool) -> [Expr]
mkEq1 (b -> b -> Bool) -> a -> a -> Bool
m = (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (\Expr
_ -> b -> Bool
forall a. Generalizable a => a -> Bool
hasEq b
x) ([Expr] -> [Expr])
-> ((a -> a -> Bool) -> [Expr]) -> (a -> a -> Bool) -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> a -> Bool) -> [Expr]
forall a. Typeable a => (a -> a -> Bool) -> [Expr]
mkEq ((a -> a -> Bool) -> [Expr]) -> (a -> a -> Bool) -> [Expr]
forall a b. (a -> b) -> a -> b
$ (b -> b -> Bool) -> a -> a -> Bool
m b -> b -> Bool
forall a. Generalizable a => a -> a -> Bool
(*==*)
  where
  x :: b
x = ((b -> b -> Bool) -> a -> a -> Bool) -> b -> b -> Bool
forall a b. (a -> b) -> a
arg1 (((b -> b -> Bool) -> a -> a -> Bool) -> b -> b -> Bool)
-> ((b -> b -> Bool) -> a -> a -> Bool) -> b
forall a b c d. (a -> b -> c -> d) -> a -> b
==: (b -> b -> Bool) -> a -> a -> Bool
m

mkEq2 :: (Generalizable a, Generalizable b, Generalizable c)
      => ((b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool) -> [Expr]
mkEq2 :: ((b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool) -> [Expr]
mkEq2 (b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool
m = (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (\Expr
_ -> b -> Bool
forall a. Generalizable a => a -> Bool
hasEq b
x Bool -> Bool -> Bool
&& c -> Bool
forall a. Generalizable a => a -> Bool
hasEq c
y) ([Expr] -> [Expr])
-> ((a -> a -> Bool) -> [Expr]) -> (a -> a -> Bool) -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> a -> Bool) -> [Expr]
forall a. Typeable a => (a -> a -> Bool) -> [Expr]
mkEq ((a -> a -> Bool) -> [Expr]) -> (a -> a -> Bool) -> [Expr]
forall a b. (a -> b) -> a -> b
$ (b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool
m b -> b -> Bool
forall a. Generalizable a => a -> a -> Bool
(*==*) c -> c -> Bool
forall a. Generalizable a => a -> a -> Bool
(*==*)
  where
  x :: b
x = ((b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool)
-> b -> b -> Bool
forall a b. (a -> b) -> a
arg1 (((b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool)
 -> b -> b -> Bool)
-> ((b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool) -> b
forall a b c d. (a -> b -> c -> d) -> a -> b
==: (b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool
m
  y :: c
y = ((b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool)
-> c -> c -> Bool
forall a b c. (a -> b -> c) -> b
arg2 (((b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool)
 -> c -> c -> Bool)
-> ((b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool) -> c
forall a b c d. (a -> b -> c -> d) -> a -> b
==: (b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool
m

mkEq3 :: (Generalizable a, Generalizable b, Generalizable c, Generalizable d)
      => ((b->b->Bool) -> (c->c->Bool) -> (d->d->Bool) -> a -> a -> Bool)
      -> [Expr]
mkEq3 :: ((b -> b -> Bool)
 -> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool)
-> [Expr]
mkEq3 (b -> b -> Bool)
-> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool
m = (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (\Expr
_ -> b -> Bool
forall a. Generalizable a => a -> Bool
hasEq b
x Bool -> Bool -> Bool
&& c -> Bool
forall a. Generalizable a => a -> Bool
hasEq c
y Bool -> Bool -> Bool
&& d -> Bool
forall a. Generalizable a => a -> Bool
hasEq d
z) ([Expr] -> [Expr])
-> ((a -> a -> Bool) -> [Expr]) -> (a -> a -> Bool) -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> a -> Bool) -> [Expr]
forall a. Typeable a => (a -> a -> Bool) -> [Expr]
mkEq
        ((a -> a -> Bool) -> [Expr]) -> (a -> a -> Bool) -> [Expr]
forall a b. (a -> b) -> a -> b
$ (b -> b -> Bool)
-> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool
m b -> b -> Bool
forall a. Generalizable a => a -> a -> Bool
(*==*) c -> c -> Bool
forall a. Generalizable a => a -> a -> Bool
(*==*) d -> d -> Bool
forall a. Generalizable a => a -> a -> Bool
(*==*)
  where
  x :: b
x = ((b -> b -> Bool)
 -> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool)
-> b -> b -> Bool
forall a b. (a -> b) -> a
arg1 (((b -> b -> Bool)
  -> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool)
 -> b -> b -> Bool)
-> ((b -> b -> Bool)
    -> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool)
-> b
forall a b c d. (a -> b -> c -> d) -> a -> b
==: (b -> b -> Bool)
-> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool
m
  y :: c
y = ((b -> b -> Bool)
 -> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool)
-> c -> c -> Bool
forall a b c. (a -> b -> c) -> b
arg2 (((b -> b -> Bool)
  -> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool)
 -> c -> c -> Bool)
-> ((b -> b -> Bool)
    -> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool)
-> c
forall a b c d. (a -> b -> c -> d) -> a -> b
==: (b -> b -> Bool)
-> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool
m
  z :: d
z = ((b -> b -> Bool)
 -> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool)
-> d -> d -> Bool
forall a b c d. (a -> b -> c -> d) -> c
arg3 (((b -> b -> Bool)
  -> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool)
 -> d -> d -> Bool)
-> ((b -> b -> Bool)
    -> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool)
-> d
forall a b c d. (a -> b -> c -> d) -> a -> b
==: (b -> b -> Bool)
-> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool
m

mkEq4 :: (Generalizable a, Generalizable b, Generalizable c, Generalizable d, Generalizable e)
      => ((b->b->Bool) -> (c->c->Bool) -> (d->d->Bool) -> (e->e->Bool) -> a -> a -> Bool)
      -> [Expr]
mkEq4 :: ((b -> b -> Bool)
 -> (c -> c -> Bool)
 -> (d -> d -> Bool)
 -> (e -> e -> Bool)
 -> a
 -> a
 -> Bool)
-> [Expr]
mkEq4 (b -> b -> Bool)
-> (c -> c -> Bool)
-> (d -> d -> Bool)
-> (e -> e -> Bool)
-> a
-> a
-> Bool
m = (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (\Expr
_ -> b -> Bool
forall a. Generalizable a => a -> Bool
hasEq b
x Bool -> Bool -> Bool
&& c -> Bool
forall a. Generalizable a => a -> Bool
hasEq c
y Bool -> Bool -> Bool
&& d -> Bool
forall a. Generalizable a => a -> Bool
hasEq d
z Bool -> Bool -> Bool
&& e -> Bool
forall a. Generalizable a => a -> Bool
hasEq e
w) ([Expr] -> [Expr])
-> ((a -> a -> Bool) -> [Expr]) -> (a -> a -> Bool) -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> a -> Bool) -> [Expr]
forall a. Typeable a => (a -> a -> Bool) -> [Expr]
mkEq
        ((a -> a -> Bool) -> [Expr]) -> (a -> a -> Bool) -> [Expr]
forall a b. (a -> b) -> a -> b
$ (b -> b -> Bool)
-> (c -> c -> Bool)
-> (d -> d -> Bool)
-> (e -> e -> Bool)
-> a
-> a
-> Bool
m b -> b -> Bool
forall a. Generalizable a => a -> a -> Bool
(*==*) c -> c -> Bool
forall a. Generalizable a => a -> a -> Bool
(*==*) d -> d -> Bool
forall a. Generalizable a => a -> a -> Bool
(*==*) e -> e -> Bool
forall a. Generalizable a => a -> a -> Bool
(*==*)
  where
  x :: b
x = ((b -> b -> Bool)
 -> (c -> c -> Bool)
 -> (d -> d -> Bool)
 -> (e -> e -> Bool)
 -> a
 -> a
 -> Bool)
-> b -> b -> Bool
forall a b. (a -> b) -> a
arg1 (((b -> b -> Bool)
  -> (c -> c -> Bool)
  -> (d -> d -> Bool)
  -> (e -> e -> Bool)
  -> a
  -> a
  -> Bool)
 -> b -> b -> Bool)
-> ((b -> b -> Bool)
    -> (c -> c -> Bool)
    -> (d -> d -> Bool)
    -> (e -> e -> Bool)
    -> a
    -> a
    -> Bool)
-> b
forall a b c d. (a -> b -> c -> d) -> a -> b
==: (b -> b -> Bool)
-> (c -> c -> Bool)
-> (d -> d -> Bool)
-> (e -> e -> Bool)
-> a
-> a
-> Bool
m
  y :: c
y = ((b -> b -> Bool)
 -> (c -> c -> Bool)
 -> (d -> d -> Bool)
 -> (e -> e -> Bool)
 -> a
 -> a
 -> Bool)
-> c -> c -> Bool
forall a b c. (a -> b -> c) -> b
arg2 (((b -> b -> Bool)
  -> (c -> c -> Bool)
  -> (d -> d -> Bool)
  -> (e -> e -> Bool)
  -> a
  -> a
  -> Bool)
 -> c -> c -> Bool)
-> ((b -> b -> Bool)
    -> (c -> c -> Bool)
    -> (d -> d -> Bool)
    -> (e -> e -> Bool)
    -> a
    -> a
    -> Bool)
-> c
forall a b c d. (a -> b -> c -> d) -> a -> b
==: (b -> b -> Bool)
-> (c -> c -> Bool)
-> (d -> d -> Bool)
-> (e -> e -> Bool)
-> a
-> a
-> Bool
m
  z :: d
z = ((b -> b -> Bool)
 -> (c -> c -> Bool)
 -> (d -> d -> Bool)
 -> (e -> e -> Bool)
 -> a
 -> a
 -> Bool)
-> d -> d -> Bool
forall a b c d. (a -> b -> c -> d) -> c
arg3 (((b -> b -> Bool)
  -> (c -> c -> Bool)
  -> (d -> d -> Bool)
  -> (e -> e -> Bool)
  -> a
  -> a
  -> Bool)
 -> d -> d -> Bool)
-> ((b -> b -> Bool)
    -> (c -> c -> Bool)
    -> (d -> d -> Bool)
    -> (e -> e -> Bool)
    -> a
    -> a
    -> Bool)
-> d
forall a b c d. (a -> b -> c -> d) -> a -> b
==: (b -> b -> Bool)
-> (c -> c -> Bool)
-> (d -> d -> Bool)
-> (e -> e -> Bool)
-> a
-> a
-> Bool
m
  w :: e
w = ((b -> b -> Bool)
 -> (c -> c -> Bool)
 -> (d -> d -> Bool)
 -> (e -> e -> Bool)
 -> a
 -> a
 -> Bool)
-> e -> e -> Bool
forall a b c d e. (a -> b -> c -> d -> e) -> d
arg4 (((b -> b -> Bool)
  -> (c -> c -> Bool)
  -> (d -> d -> Bool)
  -> (e -> e -> Bool)
  -> a
  -> a
  -> Bool)
 -> e -> e -> Bool)
-> ((b -> b -> Bool)
    -> (c -> c -> Bool)
    -> (d -> d -> Bool)
    -> (e -> e -> Bool)
    -> a
    -> a
    -> Bool)
-> e
forall a b c d. (a -> b -> c -> d) -> a -> b
==: (b -> b -> Bool)
-> (c -> c -> Bool)
-> (d -> d -> Bool)
-> (e -> e -> Bool)
-> a
-> a
-> Bool
m

mkOrd1 :: (Generalizable a, Generalizable b)
       => ((b -> b -> Bool) -> a -> a -> Bool) -> [Expr]
mkOrd1 :: ((b -> b -> Bool) -> a -> a -> Bool) -> [Expr]
mkOrd1 (b -> b -> Bool) -> a -> a -> Bool
m = (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (\Expr
_ -> b -> Bool
forall a. Generalizable a => a -> Bool
hasOrd b
x) ([Expr] -> [Expr])
-> ((a -> a -> Bool) -> [Expr]) -> (a -> a -> Bool) -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> a -> Bool) -> [Expr]
forall a. Typeable a => (a -> a -> Bool) -> [Expr]
mkOrdLessEqual
         ((a -> a -> Bool) -> [Expr]) -> (a -> a -> Bool) -> [Expr]
forall a b. (a -> b) -> a -> b
$ (b -> b -> Bool) -> a -> a -> Bool
m b -> b -> Bool
forall a. Generalizable a => a -> a -> Bool
(*<=*)
  where
  x :: b
x = ((b -> b -> Bool) -> a -> a -> Bool) -> b -> b -> Bool
forall a b. (a -> b) -> a
arg1 (((b -> b -> Bool) -> a -> a -> Bool) -> b -> b -> Bool)
-> ((b -> b -> Bool) -> a -> a -> Bool) -> b
forall a b c d. (a -> b -> c -> d) -> a -> b
==: (b -> b -> Bool) -> a -> a -> Bool
m

mkOrd2 :: (Generalizable a, Generalizable b, Generalizable c)
       => ((b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool) -> [Expr]
mkOrd2 :: ((b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool) -> [Expr]
mkOrd2 (b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool
m = (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (\Expr
_ -> b -> Bool
forall a. Generalizable a => a -> Bool
hasOrd b
x Bool -> Bool -> Bool
&& c -> Bool
forall a. Generalizable a => a -> Bool
hasOrd c
y) ([Expr] -> [Expr])
-> ((a -> a -> Bool) -> [Expr]) -> (a -> a -> Bool) -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> a -> Bool) -> [Expr]
forall a. Typeable a => (a -> a -> Bool) -> [Expr]
mkOrdLessEqual
         ((a -> a -> Bool) -> [Expr]) -> (a -> a -> Bool) -> [Expr]
forall a b. (a -> b) -> a -> b
$ (b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool
m b -> b -> Bool
forall a. Generalizable a => a -> a -> Bool
(*<=*) c -> c -> Bool
forall a. Generalizable a => a -> a -> Bool
(*<=*)
  where
  x :: b
x = ((b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool)
-> b -> b -> Bool
forall a b. (a -> b) -> a
arg1 (((b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool)
 -> b -> b -> Bool)
-> ((b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool) -> b
forall a b c d. (a -> b -> c -> d) -> a -> b
==: (b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool
m
  y :: c
y = ((b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool)
-> c -> c -> Bool
forall a b c. (a -> b -> c) -> b
arg2 (((b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool)
 -> c -> c -> Bool)
-> ((b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool) -> c
forall a b c d. (a -> b -> c -> d) -> a -> b
==: (b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool
m

mkOrd3 :: (Generalizable a, Generalizable b, Generalizable c, Generalizable d)
       => ((b->b->Bool) -> (c->c->Bool) -> (d->d->Bool) -> a -> a -> Bool)
       -> [Expr]
mkOrd3 :: ((b -> b -> Bool)
 -> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool)
-> [Expr]
mkOrd3 (b -> b -> Bool)
-> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool
m = (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (\Expr
_ -> b -> Bool
forall a. Generalizable a => a -> Bool
hasOrd b
x Bool -> Bool -> Bool
&& c -> Bool
forall a. Generalizable a => a -> Bool
hasOrd c
y Bool -> Bool -> Bool
&& d -> Bool
forall a. Generalizable a => a -> Bool
hasOrd d
z) ([Expr] -> [Expr])
-> ((a -> a -> Bool) -> [Expr]) -> (a -> a -> Bool) -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> a -> Bool) -> [Expr]
forall a. Typeable a => (a -> a -> Bool) -> [Expr]
mkOrdLessEqual
         ((a -> a -> Bool) -> [Expr]) -> (a -> a -> Bool) -> [Expr]
forall a b. (a -> b) -> a -> b
$ (b -> b -> Bool)
-> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool
m b -> b -> Bool
forall a. Generalizable a => a -> a -> Bool
(*<=*) c -> c -> Bool
forall a. Generalizable a => a -> a -> Bool
(*<=*) d -> d -> Bool
forall a. Generalizable a => a -> a -> Bool
(*<=*)
  where
  x :: b
x = ((b -> b -> Bool)
 -> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool)
-> b -> b -> Bool
forall a b. (a -> b) -> a
arg1 (((b -> b -> Bool)
  -> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool)
 -> b -> b -> Bool)
-> ((b -> b -> Bool)
    -> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool)
-> b
forall a b c d. (a -> b -> c -> d) -> a -> b
==: (b -> b -> Bool)
-> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool
m
  y :: c
y = ((b -> b -> Bool)
 -> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool)
-> c -> c -> Bool
forall a b c. (a -> b -> c) -> b
arg2 (((b -> b -> Bool)
  -> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool)
 -> c -> c -> Bool)
-> ((b -> b -> Bool)
    -> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool)
-> c
forall a b c d. (a -> b -> c -> d) -> a -> b
==: (b -> b -> Bool)
-> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool
m
  z :: d
z = ((b -> b -> Bool)
 -> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool)
-> d -> d -> Bool
forall a b c d. (a -> b -> c -> d) -> c
arg3 (((b -> b -> Bool)
  -> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool)
 -> d -> d -> Bool)
-> ((b -> b -> Bool)
    -> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool)
-> d
forall a b c d. (a -> b -> c -> d) -> a -> b
==: (b -> b -> Bool)
-> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool
m

mkOrd4 :: (Generalizable a, Generalizable b, Generalizable c, Generalizable d, Generalizable e)
       => ((b->b->Bool) -> (c->c->Bool) -> (d->d->Bool) -> (e->e->Bool) -> a -> a -> Bool)
       -> [Expr]
mkOrd4 :: ((b -> b -> Bool)
 -> (c -> c -> Bool)
 -> (d -> d -> Bool)
 -> (e -> e -> Bool)
 -> a
 -> a
 -> Bool)
-> [Expr]
mkOrd4 (b -> b -> Bool)
-> (c -> c -> Bool)
-> (d -> d -> Bool)
-> (e -> e -> Bool)
-> a
-> a
-> Bool
m = (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (\Expr
_ -> b -> Bool
forall a. Generalizable a => a -> Bool
hasOrd b
x Bool -> Bool -> Bool
&& c -> Bool
forall a. Generalizable a => a -> Bool
hasOrd c
y Bool -> Bool -> Bool
&& d -> Bool
forall a. Generalizable a => a -> Bool
hasOrd d
z Bool -> Bool -> Bool
&& e -> Bool
forall a. Generalizable a => a -> Bool
hasOrd e
w) ([Expr] -> [Expr])
-> ((a -> a -> Bool) -> [Expr]) -> (a -> a -> Bool) -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> a -> Bool) -> [Expr]
forall a. Typeable a => (a -> a -> Bool) -> [Expr]
mkOrdLessEqual
         ((a -> a -> Bool) -> [Expr]) -> (a -> a -> Bool) -> [Expr]
forall a b. (a -> b) -> a -> b
$ (b -> b -> Bool)
-> (c -> c -> Bool)
-> (d -> d -> Bool)
-> (e -> e -> Bool)
-> a
-> a
-> Bool
m b -> b -> Bool
forall a. Generalizable a => a -> a -> Bool
(*<=*) c -> c -> Bool
forall a. Generalizable a => a -> a -> Bool
(*<=*) d -> d -> Bool
forall a. Generalizable a => a -> a -> Bool
(*<=*) e -> e -> Bool
forall a. Generalizable a => a -> a -> Bool
(*<=*)
  where
  x :: b
x = ((b -> b -> Bool)
 -> (c -> c -> Bool)
 -> (d -> d -> Bool)
 -> (e -> e -> Bool)
 -> a
 -> a
 -> Bool)
-> b -> b -> Bool
forall a b. (a -> b) -> a
arg1 (((b -> b -> Bool)
  -> (c -> c -> Bool)
  -> (d -> d -> Bool)
  -> (e -> e -> Bool)
  -> a
  -> a
  -> Bool)
 -> b -> b -> Bool)
-> ((b -> b -> Bool)
    -> (c -> c -> Bool)
    -> (d -> d -> Bool)
    -> (e -> e -> Bool)
    -> a
    -> a
    -> Bool)
-> b
forall a b c d. (a -> b -> c -> d) -> a -> b
==: (b -> b -> Bool)
-> (c -> c -> Bool)
-> (d -> d -> Bool)
-> (e -> e -> Bool)
-> a
-> a
-> Bool
m
  y :: c
y = ((b -> b -> Bool)
 -> (c -> c -> Bool)
 -> (d -> d -> Bool)
 -> (e -> e -> Bool)
 -> a
 -> a
 -> Bool)
-> c -> c -> Bool
forall a b c. (a -> b -> c) -> b
arg2 (((b -> b -> Bool)
  -> (c -> c -> Bool)
  -> (d -> d -> Bool)
  -> (e -> e -> Bool)
  -> a
  -> a
  -> Bool)
 -> c -> c -> Bool)
-> ((b -> b -> Bool)
    -> (c -> c -> Bool)
    -> (d -> d -> Bool)
    -> (e -> e -> Bool)
    -> a
    -> a
    -> Bool)
-> c
forall a b c d. (a -> b -> c -> d) -> a -> b
==: (b -> b -> Bool)
-> (c -> c -> Bool)
-> (d -> d -> Bool)
-> (e -> e -> Bool)
-> a
-> a
-> Bool
m
  z :: d
z = ((b -> b -> Bool)
 -> (c -> c -> Bool)
 -> (d -> d -> Bool)
 -> (e -> e -> Bool)
 -> a
 -> a
 -> Bool)
-> d -> d -> Bool
forall a b c d. (a -> b -> c -> d) -> c
arg3 (((b -> b -> Bool)
  -> (c -> c -> Bool)
  -> (d -> d -> Bool)
  -> (e -> e -> Bool)
  -> a
  -> a
  -> Bool)
 -> d -> d -> Bool)
-> ((b -> b -> Bool)
    -> (c -> c -> Bool)
    -> (d -> d -> Bool)
    -> (e -> e -> Bool)
    -> a
    -> a
    -> Bool)
-> d
forall a b c d. (a -> b -> c -> d) -> a -> b
==: (b -> b -> Bool)
-> (c -> c -> Bool)
-> (d -> d -> Bool)
-> (e -> e -> Bool)
-> a
-> a
-> Bool
m
  w :: e
w = ((b -> b -> Bool)
 -> (c -> c -> Bool)
 -> (d -> d -> Bool)
 -> (e -> e -> Bool)
 -> a
 -> a
 -> Bool)
-> e -> e -> Bool
forall a b c d e. (a -> b -> c -> d -> e) -> d
arg4 (((b -> b -> Bool)
  -> (c -> c -> Bool)
  -> (d -> d -> Bool)
  -> (e -> e -> Bool)
  -> a
  -> a
  -> Bool)
 -> e -> e -> Bool)
-> ((b -> b -> Bool)
    -> (c -> c -> Bool)
    -> (d -> d -> Bool)
    -> (e -> e -> Bool)
    -> a
    -> a
    -> Bool)
-> e
forall a b c d. (a -> b -> c -> d) -> a -> b
==: (b -> b -> Bool)
-> (c -> c -> Bool)
-> (d -> d -> Bool)
-> (e -> e -> Bool)
-> a
-> a
-> Bool
m

-- | Usage: @ins "x" (undefined :: Type)@
ins :: Generalizable a => a -> Instances
ins :: a -> [Expr]
ins a
x = a -> [Expr]
forall a. (Typeable a, Show a, Listable a) => a -> [Expr]
reifyListable a
x
     [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ a -> [Expr]
forall a. (Typeable a, Name a) => a -> [Expr]
reifyName a
x
     [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ a -> [Expr]
forall a. Generalizable a => a -> [Expr]
reifyBackground a
x

-- | Used in the definition of 'subInstances'
--   in 'Generalizable' typeclass instances.
instances :: Generalizable a => a -> Instances -> Instances
instances :: a -> [Expr] -> [Expr]
instances a
x = a -> ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a.
Generalizable a =>
a -> ([Expr] -> [Expr]) -> [Expr] -> [Expr]
this a
x (a -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
subInstances a
x)
  where
  this :: Generalizable a
       => a -> (Instances -> Instances) -> Instances -> Instances
  this :: a -> ([Expr] -> [Expr]) -> [Expr] -> [Expr]
this a
x [Expr] -> [Expr]
f [Expr]
is =
    if [Expr] -> TypeRep -> Bool
isListableT [Expr]
is (a -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf a
x)
      then [Expr]
is
      else [Expr] -> [Expr]
f (a -> [Expr]
forall a. Generalizable a => a -> [Expr]
ins a
x [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr]
is)
  -- TODO: change type to a -> [Instances -> Instances] -> Instances -> Instances

reifyBackground :: Generalizable a => a -> Instances
reifyBackground :: a -> [Expr]
reifyBackground a
x = [String -> [Expr] -> Expr
forall a. Typeable a => String -> a -> Expr
value String
"background" (a -> [Expr]
forall a. Generalizable a => a -> [Expr]
background a
x)]

fromBackgroundOf :: (Generalizable a, Typeable b) => String -> a -> Maybe b
fromBackgroundOf :: String -> a -> Maybe b
fromBackgroundOf String
nm = [b] -> Maybe b
forall a. [a] -> Maybe a
listToMaybe
                    ([b] -> Maybe b) -> (a -> [b]) -> a -> Maybe b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Maybe b) -> [Expr] -> [b]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Expr -> Maybe b
forall a. Typeable a => Expr -> Maybe a
evaluate
                    ([Expr] -> [b]) -> (a -> [Expr]) -> a -> [b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
filter (Expr -> String -> Bool
`isConstantNamed` String
nm)
                    ([Expr] -> [Expr]) -> (a -> [Expr]) -> a -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> [Expr]
forall a. Generalizable a => a -> [Expr]
background

hasEq :: Generalizable a => a -> Bool
hasEq :: a -> Bool
hasEq a
x = Maybe (a -> a -> Bool) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (a -> a -> Bool) -> Bool) -> Maybe (a -> a -> Bool) -> Bool
forall a b. (a -> b) -> a -> b
$ String
"==" String -> a -> Maybe (a -> a -> Bool)
forall a b. (Generalizable a, Typeable b) => String -> a -> Maybe b
`fromBackgroundOf` a
x Maybe (a -> a -> Bool)
-> Maybe (a -> a -> Bool) -> Maybe (a -> a -> Bool)
forall a. a -> a -> a
-: (a -> a -> Bool) -> Maybe (a -> a -> Bool)
forall a. a -> Maybe a
mayb (a
x a -> (a -> Bool) -> a -> a -> Bool
forall a b. a -> b -> a -> b
>- a
x a -> Bool -> a -> Bool
forall a b. a -> b -> a -> b
>- Bool
bool)

hasOrd :: Generalizable a => a -> Bool
hasOrd :: a -> Bool
hasOrd a
x = Maybe (a -> a -> Bool) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (a -> a -> Bool) -> Bool) -> Maybe (a -> a -> Bool) -> Bool
forall a b. (a -> b) -> a -> b
$ String
"<=" String -> a -> Maybe (a -> a -> Bool)
forall a b. (Generalizable a, Typeable b) => String -> a -> Maybe b
`fromBackgroundOf` a
x Maybe (a -> a -> Bool)
-> Maybe (a -> a -> Bool) -> Maybe (a -> a -> Bool)
forall a. a -> a -> a
-: (a -> a -> Bool) -> Maybe (a -> a -> Bool)
forall a. a -> Maybe a
mayb (a
x a -> (a -> Bool) -> a -> a -> Bool
forall a b. a -> b -> a -> b
>- a
x a -> Bool -> a -> Bool
forall a b. a -> b -> a -> b
>- Bool
bool)

(*==*) :: Generalizable a => a -> a -> Bool
a
x *==* :: a -> a -> Bool
*==* a
y = a
x a -> a -> Bool
== a
y
  where
  == :: a -> a -> Bool
(==) = (a -> a -> Bool) -> Maybe (a -> a -> Bool) -> a -> a -> Bool
forall a. a -> Maybe a -> a
fromMaybe (String -> a -> a -> Bool
forall a. HasCallStack => String -> a
error String
"(*==*): no (==) operator in background")
       (Maybe (a -> a -> Bool) -> a -> a -> Bool)
-> Maybe (a -> a -> Bool) -> a -> a -> Bool
forall a b. (a -> b) -> a -> b
$ String
"==" String -> a -> Maybe (a -> a -> Bool)
forall a b. (Generalizable a, Typeable b) => String -> a -> Maybe b
`fromBackgroundOf` a
x

(*/=*) :: Generalizable a => a -> a -> Bool
a
x */=* :: a -> a -> Bool
*/=* a
y = a
x a -> a -> Bool
/= a
y
  where
  /= :: a -> a -> Bool
(/=) = (a -> a -> Bool) -> Maybe (a -> a -> Bool) -> a -> a -> Bool
forall a. a -> Maybe a -> a
fromMaybe (String -> a -> a -> Bool
forall a. HasCallStack => String -> a
error String
"(*/=*): no (/=) operator in background")
       (Maybe (a -> a -> Bool) -> a -> a -> Bool)
-> Maybe (a -> a -> Bool) -> a -> a -> Bool
forall a b. (a -> b) -> a -> b
$ String
"/=" String -> a -> Maybe (a -> a -> Bool)
forall a b. (Generalizable a, Typeable b) => String -> a -> Maybe b
`fromBackgroundOf` a
x

(*<=*) :: Generalizable a => a -> a -> Bool
a
x *<=* :: a -> a -> Bool
*<=* a
y = a
x a -> a -> Bool
<= a
y
  where
  <= :: a -> a -> Bool
(<=) = (a -> a -> Bool) -> Maybe (a -> a -> Bool) -> a -> a -> Bool
forall a. a -> Maybe a -> a
fromMaybe (String -> a -> a -> Bool
forall a. HasCallStack => String -> a
error String
"(*<=*): no (<=) operator in background")
       (Maybe (a -> a -> Bool) -> a -> a -> Bool)
-> Maybe (a -> a -> Bool) -> a -> a -> Bool
forall a b. (a -> b) -> a -> b
$ String
"<=" String -> a -> Maybe (a -> a -> Bool)
forall a b. (Generalizable a, Typeable b) => String -> a -> Maybe b
`fromBackgroundOf` a
x

(*<*) :: Generalizable a => a -> a -> Bool
a
x *<* :: a -> a -> Bool
*<* a
y = a
x a -> a -> Bool
< a
y
  where
  < :: a -> a -> Bool
(<) = (a -> a -> Bool) -> Maybe (a -> a -> Bool) -> a -> a -> Bool
forall a. a -> Maybe a -> a
fromMaybe (String -> a -> a -> Bool
forall a. HasCallStack => String -> a
error String
"(*<*): no (<) operator in background")
       (Maybe (a -> a -> Bool) -> a -> a -> Bool)
-> Maybe (a -> a -> Bool) -> a -> a -> Bool
forall a b. (a -> b) -> a -> b
$ String
"<" String -> a -> Maybe (a -> a -> Bool)
forall a b. (Generalizable a, Typeable b) => String -> a -> Maybe b
`fromBackgroundOf` a
x

-- -- other Generalizable instances -- --

instance (Integral a, Generalizable a) => Generalizable (Ratio a)

instance ( Generalizable a, Generalizable b, Generalizable c, Generalizable d
         , Generalizable e )
      => Generalizable (a,b,c,d,e) where
  subInstances :: (a, b, c, d, e) -> [Expr] -> [Expr]
subInstances (a, b, c, d, e)
xyzwv = a -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances a
x ([Expr] -> [Expr]) -> ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances b
y ([Expr] -> [Expr]) -> ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances c
z
                     ([Expr] -> [Expr]) -> ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. d -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances d
w ([Expr] -> [Expr]) -> ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances e
v
                     where (a
x,b
y,c
z,d
w,e
v) = (a, b, c, d, e)
xyzwv

instance ( Generalizable a, Generalizable b, Generalizable c, Generalizable d
         , Generalizable e, Generalizable f )
      => Generalizable (a,b,c,d,e,f) where
  subInstances :: (a, b, c, d, e, f) -> [Expr] -> [Expr]
subInstances (a, b, c, d, e, f)
xyzwvu = a -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances a
x ([Expr] -> [Expr]) -> ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances b
y ([Expr] -> [Expr]) -> ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances c
z
                      ([Expr] -> [Expr]) -> ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. d -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances d
w ([Expr] -> [Expr]) -> ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances e
v ([Expr] -> [Expr]) -> ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances f
u
               where (a
x,b
y,c
z,d
w,e
v,f
u) = (a, b, c, d, e, f)
xyzwvu

instance ( Generalizable a, Generalizable b, Generalizable c, Generalizable d
         , Generalizable e, Generalizable f, Generalizable g )
      => Generalizable (a,b,c,d,e,f,g) where
  subInstances :: (a, b, c, d, e, f, g) -> [Expr] -> [Expr]
subInstances (a, b, c, d, e, f, g)
xyzwvut = a -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances a
x ([Expr] -> [Expr]) -> ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances b
y ([Expr] -> [Expr]) -> ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances c
z ([Expr] -> [Expr]) -> ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. d -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances d
w
                       ([Expr] -> [Expr]) -> ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances e
v ([Expr] -> [Expr]) -> ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances f
u ([Expr] -> [Expr]) -> ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances g
t
                where (a
x,b
y,c
z,d
w,e
v,f
u,g
t) = (a, b, c, d, e, f, g)
xyzwvut

#if __GLASGOW_HASKELL__ < 710
-- No 8-tuples for you:
-- On GHC 7.8, 8-tuples are not Typeable instances.  We could add a standalone
-- deriving clause, but that may cause trouble if some other library does the
-- same.  User should declare Generalizable 8-tuples manually when using GHC <=
-- 7.8.
#else
instance ( Generalizable a, Generalizable b, Generalizable c, Generalizable d
         , Generalizable e, Generalizable f, Generalizable g, Generalizable h )
      => Generalizable (a,b,c,d,e,f,g,h) where
  subInstances :: (a, b, c, d, e, f, g, h) -> [Expr] -> [Expr]
subInstances (a, b, c, d, e, f, g, h)
xyzwvuts = a -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances a
x ([Expr] -> [Expr]) -> ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances b
y ([Expr] -> [Expr]) -> ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances c
z ([Expr] -> [Expr]) -> ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. d -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances d
w
                        ([Expr] -> [Expr]) -> ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances e
v ([Expr] -> [Expr]) -> ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances f
u ([Expr] -> [Expr]) -> ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances g
t ([Expr] -> [Expr]) -> ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. h -> [Expr] -> [Expr]
forall a. Generalizable a => a -> [Expr] -> [Expr]
instances h
s
    where (a
x,b
y,c
z,d
w,e
v,f
u,g
t,h
s) = (a, b, c, d, e, f, g, h)
xyzwvuts
#endif