-- | Useful operations on terms and similar. Also re-exports some generally
-- useful modules such as 'Twee.Term' and 'Twee.Pretty'.

{-# LANGUAGE TypeFamilies, FlexibleInstances, UndecidableInstances, DeriveFunctor, DefaultSignatures, FlexibleContexts, TypeOperators, MultiParamTypeClasses, GeneralizedNewtypeDeriving, ConstraintKinds, RecordWildCards #-}
module Twee.Base(
  -- * Re-exported functionality
  module Twee.Term, module Twee.Pretty,
  -- * The 'Symbolic' typeclass
  Symbolic(..), subst, terms,
  TermOf, TermListOf, SubstOf, TriangleSubstOf, BuilderOf, FunOf,
  vars, isGround, funs, occ, occVar, canonicalise, renameAvoiding, renameManyAvoiding, freshVar,
  -- * General-purpose functionality
  Id(..), Has(..),
  -- * Typeclasses
  Minimal(..), minimalTerm, isMinimal, erase, eraseExcept, ground,
  Ordered(..), lessThan, orientTerms, EqualsBonus(..), Strictness(..), Function) where

import Prelude hiding (lookup)
import Control.Monad
import qualified Data.DList as DList
import Twee.Term hiding (subst, canonicalise)
import qualified Twee.Term as Term
import Twee.Utils
import Twee.Pretty
import Twee.Constraints hiding (funs)
import Data.DList(DList)
import Data.Int
import Data.List hiding (singleton)
import Data.Maybe
import qualified Data.IntMap.Strict as IntMap
import Data.Serialize

-- | Represents a unique identifier (e.g., for a rule).
newtype Id = Id { Id -> Int32
unId :: Int32 }
  deriving (Id -> Id -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Id -> Id -> Bool
$c/= :: Id -> Id -> Bool
== :: Id -> Id -> Bool
$c== :: Id -> Id -> Bool
Eq, Eq Id
Id -> Id -> Bool
Id -> Id -> Ordering
Id -> Id -> Id
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Id -> Id -> Id
$cmin :: Id -> Id -> Id
max :: Id -> Id -> Id
$cmax :: Id -> Id -> Id
>= :: Id -> Id -> Bool
$c>= :: Id -> Id -> Bool
> :: Id -> Id -> Bool
$c> :: Id -> Id -> Bool
<= :: Id -> Id -> Bool
$c<= :: Id -> Id -> Bool
< :: Id -> Id -> Bool
$c< :: Id -> Id -> Bool
compare :: Id -> Id -> Ordering
$ccompare :: Id -> Id -> Ordering
Ord, Int -> Id -> ShowS
[Id] -> ShowS
Id -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Id] -> ShowS
$cshowList :: [Id] -> ShowS
show :: Id -> String
$cshow :: Id -> String
showsPrec :: Int -> Id -> ShowS
$cshowsPrec :: Int -> Id -> ShowS
Show, Int -> Id
Id -> Int
Id -> [Id]
Id -> Id
Id -> Id -> [Id]
Id -> Id -> Id -> [Id]
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: Id -> Id -> Id -> [Id]
$cenumFromThenTo :: Id -> Id -> Id -> [Id]
enumFromTo :: Id -> Id -> [Id]
$cenumFromTo :: Id -> Id -> [Id]
enumFromThen :: Id -> Id -> [Id]
$cenumFromThen :: Id -> Id -> [Id]
enumFrom :: Id -> [Id]
$cenumFrom :: Id -> [Id]
fromEnum :: Id -> Int
$cfromEnum :: Id -> Int
toEnum :: Int -> Id
$ctoEnum :: Int -> Id
pred :: Id -> Id
$cpred :: Id -> Id
succ :: Id -> Id
$csucc :: Id -> Id
Enum, Id
forall a. a -> a -> Bounded a
maxBound :: Id
$cmaxBound :: Id
minBound :: Id
$cminBound :: Id
Bounded, Integer -> Id
Id -> Id
Id -> Id -> Id
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
fromInteger :: Integer -> Id
$cfromInteger :: Integer -> Id
signum :: Id -> Id
$csignum :: Id -> Id
abs :: Id -> Id
$cabs :: Id -> Id
negate :: Id -> Id
$cnegate :: Id -> Id
* :: Id -> Id -> Id
$c* :: Id -> Id -> Id
- :: Id -> Id -> Id
$c- :: Id -> Id -> Id
+ :: Id -> Id -> Id
$c+ :: Id -> Id -> Id
Num, Num Id
Ord Id
Id -> Rational
forall a. Num a -> Ord a -> (a -> Rational) -> Real a
toRational :: Id -> Rational
$ctoRational :: Id -> Rational
Real, Enum Id
Real Id
Id -> Integer
Id -> Id -> (Id, Id)
Id -> Id -> Id
forall a.
Real a
-> Enum a
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> (a, a))
-> (a -> a -> (a, a))
-> (a -> Integer)
-> Integral a
toInteger :: Id -> Integer
$ctoInteger :: Id -> Integer
divMod :: Id -> Id -> (Id, Id)
$cdivMod :: Id -> Id -> (Id, Id)
quotRem :: Id -> Id -> (Id, Id)
$cquotRem :: Id -> Id -> (Id, Id)
mod :: Id -> Id -> Id
$cmod :: Id -> Id -> Id
div :: Id -> Id -> Id
$cdiv :: Id -> Id -> Id
rem :: Id -> Id -> Id
$crem :: Id -> Id -> Id
quot :: Id -> Id -> Id
$cquot :: Id -> Id -> Id
Integral, Get Id
Putter Id
forall t. Putter t -> Get t -> Serialize t
get :: Get Id
$cget :: Get Id
put :: Putter Id
$cput :: Putter Id
Serialize)

instance Pretty Id where
  pPrint :: Id -> Doc
pPrint = String -> Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Int32
unId

-- | Generalisation of term functionality to things that contain terms (e.g.,
-- rewrite rules and equations).
class Symbolic a where
  type ConstantOf a

  -- | Compute a 'DList' of all terms which appear in the argument
  -- (used for e.g. computing free variables).
  -- See also 'terms'.
  termsDL :: a -> DList (TermListOf a)

  -- | Apply a substitution.
  -- When using the 'Symbolic' type class, you can use 'subst' instead.
  subst_ :: (Var -> BuilderOf a) -> a -> a

-- | Apply a substitution.
subst :: (Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) => s -> a -> a
subst :: forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst s
sub a
x = forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ (forall s. Substitution s => s -> Var -> Builder (SubstFun s)
evalSubst s
sub) a
x

-- | Find all terms occuring in the argument.
terms :: Symbolic a => a -> [TermListOf a]
terms :: forall a. Symbolic a => a -> [TermListOf a]
terms = forall a. DList a -> [a]
DList.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Symbolic a => a -> DList (TermListOf a)
termsDL

-- | A term compatible with a given 'Symbolic'.
type TermOf a = Term (ConstantOf a)
-- | A termlist compatible with a given 'Symbolic'.
type TermListOf a = TermList (ConstantOf a)
-- | A substitution compatible with a given 'Symbolic'.
type SubstOf a = Subst (ConstantOf a)
-- | A triangle substitution compatible with a given 'Symbolic'.
type TriangleSubstOf a = TriangleSubst (ConstantOf a)
-- | A builder compatible with a given 'Symbolic'.
type BuilderOf a = Builder (ConstantOf a)
-- | The underlying type of function symbols of a given 'Symbolic'.
type FunOf a = Fun (ConstantOf a)

instance Symbolic (Term f) where
  type ConstantOf (Term f) = f
  termsDL :: Term f -> DList (TermListOf (Term f))
termsDL = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. Term f -> TermList f
singleton
  subst_ :: (Var -> BuilderOf (Term f)) -> Term f -> Term f
subst_ Var -> BuilderOf (Term f)
sub = forall a. Build a => a -> Term (BuildFun a)
build forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s.
Substitution s =>
s -> Term (SubstFun s) -> Builder (SubstFun s)
Term.subst Var -> BuilderOf (Term f)
sub

instance Symbolic (TermList f) where
  type ConstantOf (TermList f) = f
  termsDL :: TermList f -> DList (TermListOf (TermList f))
termsDL = forall (m :: * -> *) a. Monad m => a -> m a
return
  subst_ :: (Var -> BuilderOf (TermList f)) -> TermList f -> TermList f
subst_ Var -> BuilderOf (TermList f)
sub = forall a. Build a => a -> TermList (BuildFun a)
buildList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s.
Substitution s =>
s -> TermList (SubstFun s) -> Builder (SubstFun s)
Term.substList Var -> BuilderOf (TermList f)
sub

instance Symbolic (Subst f) where
  type ConstantOf (Subst f) = f
  termsDL :: Subst f -> DList (TermListOf (Subst f))
termsDL (Subst IntMap (TermList f)
sub) = forall a. Symbolic a => a -> DList (TermListOf a)
termsDL (forall a. IntMap a -> [a]
IntMap.elems IntMap (TermList f)
sub)
  subst_ :: (Var -> BuilderOf (Subst f)) -> Subst f -> Subst f
subst_ Var -> BuilderOf (Subst f)
sub (Subst IntMap (TermList f)
s) = forall f. IntMap (TermList f) -> Subst f
Subst (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (Subst f)
sub) IntMap (TermList f)
s)

instance (ConstantOf a ~ ConstantOf b, Symbolic a, Symbolic b) => Symbolic (a, b) where
  type ConstantOf (a, b) = ConstantOf a
  termsDL :: (a, b) -> DList (TermListOf (a, b))
termsDL (a
x, b
y) = forall a. Symbolic a => a -> DList (TermListOf a)
termsDL a
x forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` forall a. Symbolic a => a -> DList (TermListOf a)
termsDL b
y
  subst_ :: (Var -> BuilderOf (a, b)) -> (a, b) -> (a, b)
subst_ Var -> BuilderOf (a, b)
sub (a
x, b
y) = (forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (a, b)
sub a
x, forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (a, b)
sub b
y)

instance (ConstantOf a ~ ConstantOf b,
          ConstantOf a ~ ConstantOf c,
          Symbolic a, Symbolic b, Symbolic c) => Symbolic (a, b, c) where
  type ConstantOf (a, b, c) = ConstantOf a
  termsDL :: (a, b, c) -> DList (TermListOf (a, b, c))
termsDL (a
x, b
y, c
z) = forall a. Symbolic a => a -> DList (TermListOf a)
termsDL a
x forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` forall a. Symbolic a => a -> DList (TermListOf a)
termsDL b
y forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` forall a. Symbolic a => a -> DList (TermListOf a)
termsDL c
z
  subst_ :: (Var -> BuilderOf (a, b, c)) -> (a, b, c) -> (a, b, c)
subst_ Var -> BuilderOf (a, b, c)
sub (a
x, b
y, c
z) = (forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (a, b, c)
sub a
x, forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (a, b, c)
sub b
y, forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (a, b, c)
sub c
z)

instance Symbolic a => Symbolic [a] where
  type ConstantOf [a] = ConstantOf a
  termsDL :: [a] -> DList (TermListOf [a])
termsDL [a]
xs = forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum (forall a b. (a -> b) -> [a] -> [b]
map forall a. Symbolic a => a -> DList (TermListOf a)
termsDL [a]
xs)
  subst_ :: (Var -> BuilderOf [a]) -> [a] -> [a]
subst_ Var -> BuilderOf [a]
sub [a]
xs = forall a b. (a -> b) -> [a] -> [b]
map (forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf [a]
sub) [a]
xs

instance Symbolic a => Symbolic (Maybe a) where
  type ConstantOf (Maybe a) = ConstantOf a
  termsDL :: Maybe a -> DList (TermListOf (Maybe a))
termsDL Maybe a
Nothing = forall (m :: * -> *) a. MonadPlus m => m a
mzero
  termsDL (Just a
x) = forall a. Symbolic a => a -> DList (TermListOf a)
termsDL a
x
  subst_ :: (Var -> BuilderOf (Maybe a)) -> Maybe a -> Maybe a
subst_ Var -> BuilderOf (Maybe a)
sub Maybe a
x = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (Maybe a)
sub) Maybe a
x

-- | An instance @'Has' a b@ indicates that a value of type @a@ contains a value
-- of type @b@ which is somehow part of the meaning of the @a@.
--
-- A number of functions use 'Has' constraints to work in a more general setting.
-- For example, the functions in 'Twee.CP' operate on rewrite rules, but actually
-- accept any @a@ satisfying @'Has' a ('Twee.Rule.Rule' f)@.
--
-- Use taste when definining 'Has' instances; don't do it willy-nilly.
class Has a b where
  -- | Get at the thing.
  the :: a -> b

-- | Find the variables occurring in the argument.
{-# INLINE vars #-}
vars :: Symbolic a => a -> [Var]
vars :: forall a. Symbolic a => a -> [Var]
vars a
x = [ Var
v | TermList (ConstantOf a)
t <- forall a. DList a -> [a]
DList.toList (forall a. Symbolic a => a -> DList (TermListOf a)
termsDL a
x), Var Var
v <- forall f. TermList f -> [Term f]
subtermsList TermList (ConstantOf a)
t ]

-- | Test if the argument is ground.
{-# INLINE isGround #-}
isGround :: Symbolic a => a -> Bool
isGround :: forall a. Symbolic a => a -> Bool
isGround = forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Symbolic a => a -> [Var]
vars

-- | Find the function symbols occurring in the argument.
{-# INLINE funs #-}
funs :: Symbolic a => a -> [FunOf a]
funs :: forall a. Symbolic a => a -> [FunOf a]
funs a
x = [ FunOf a
f | TermList (ConstantOf a)
t <- forall a. DList a -> [a]
DList.toList (forall a. Symbolic a => a -> DList (TermListOf a)
termsDL a
x), App FunOf a
f TermList (ConstantOf a)
_ <- forall f. TermList f -> [Term f]
subtermsList TermList (ConstantOf a)
t ]

-- | Count how many times a function symbol occurs in the argument.
{-# INLINE occ #-}
occ :: Symbolic a => FunOf a -> a -> Int
occ :: forall a. Symbolic a => FunOf a -> a -> Int
occ FunOf a
x a
t = forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => a -> a -> Bool
== FunOf a
x) (forall a. Symbolic a => a -> [FunOf a]
funs a
t))

-- | Count how many times a variable occurs in the argument.
{-# INLINE occVar #-}
occVar :: Symbolic a => Var -> a -> Int
occVar :: forall a. Symbolic a => Var -> a -> Int
occVar Var
x a
t = forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => a -> a -> Bool
== Var
x) (forall a. Symbolic a => a -> [Var]
vars a
t))

-- | Rename the argument so that variables are introduced in a canonical order
-- (starting with V0, then V1 and so on).
{-# INLINEABLE canonicalise #-}
canonicalise :: Symbolic a => a -> a
canonicalise :: forall a. Symbolic a => a -> a
canonicalise a
t = forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst (ConstantOf a)
sub a
t
  where
    sub :: Subst (ConstantOf a)
sub = forall f. [TermList f] -> Subst f
Term.canonicalise (forall a. DList a -> [a]
DList.toList (forall a. Symbolic a => a -> DList (TermListOf a)
termsDL a
t))

-- | Rename the second argument so that it does not mention any variable which
-- occurs in the first.
{-# INLINEABLE renameAvoiding #-}
renameAvoiding :: (Symbolic a, Symbolic b) => a -> b -> b
renameAvoiding :: forall a b. (Symbolic a, Symbolic b) => a -> b -> b
renameAvoiding a
x b
y
  | Int
x2 forall a. Ord a => a -> a -> Bool
< Int
y1 Bool -> Bool -> Bool
|| Int
y2 forall a. Ord a => a -> a -> Bool
< Int
x1 =
    -- No overlap. Important in the case when x is ground,
    -- in which case x2 == minBound and the calculation below doesn't work.
    b
y
  | Bool
otherwise =
    -- Map y1 to x2+1
    forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst (\(V Int
x) -> forall f. Var -> Builder f
var (Int -> Var
V (Int
xforall a. Num a => a -> a -> a
-Int
y1forall a. Num a => a -> a -> a
+Int
x2forall a. Num a => a -> a -> a
+Int
1))) b
y
  where
    (V Int
x1, V Int
x2) = forall f. [TermList f] -> (Var, Var)
boundLists (forall a. Symbolic a => a -> [TermListOf a]
terms a
x)
    (V Int
y1, V Int
y2) = forall f. [TermList f] -> (Var, Var)
boundLists (forall a. Symbolic a => a -> [TermListOf a]
terms b
y)

-- | Return an x such that no variable >= x occurs in the argument.
freshVar :: Symbolic a => a -> Int
freshVar :: forall a. Symbolic a => a -> Int
freshVar a
x
  | Int
x1 forall a. Ord a => a -> a -> Bool
> Int
x2 = Int
0 -- x is ground
  | Bool
otherwise = Int
x2forall a. Num a => a -> a -> a
+Int
1
  where
    (V Int
x1, V Int
x2) = forall f. [TermList f] -> (Var, Var)
boundLists (forall a. Symbolic a => a -> [TermListOf a]
terms a
x)

{-# INLINEABLE renameManyAvoiding #-}
renameManyAvoiding :: Symbolic a => [a] -> [a]
renameManyAvoiding :: forall a. Symbolic a => [a] -> [a]
renameManyAvoiding [] = []
renameManyAvoiding (a
t:[a]
ts) = a
uforall a. a -> [a] -> [a]
:[a]
us
  where
    u :: a
u = forall a b. (Symbolic a, Symbolic b) => a -> b -> b
renameAvoiding [a]
us a
t
    us :: [a]
us = forall a. Symbolic a => [a] -> [a]
renameManyAvoiding [a]
ts
  
-- | Check if a term is the minimal constant.
isMinimal :: Minimal f => Term f -> Bool
isMinimal :: forall f. Minimal f => Term f -> Bool
isMinimal (App Fun f
f TermList f
Empty) | Fun f
f forall a. Eq a => a -> a -> Bool
== forall f. Minimal f => Fun f
minimal = Bool
True
isMinimal Term f
_ = Bool
False

-- | Build the minimal constant as a term.
minimalTerm :: Minimal f => Term f
minimalTerm :: forall f. Minimal f => Term f
minimalTerm = forall a. Build a => a -> Term (BuildFun a)
build (forall f. Fun f -> Builder f
con forall f. Minimal f => Fun f
minimal)

-- | Erase a given set of variables from the argument, replacing them with the
-- minimal constant.
erase :: (Symbolic a, ConstantOf a ~ f, Minimal f) => [Var] -> a -> a
erase :: forall a f.
(Symbolic a, ConstantOf a ~ f, Minimal f) =>
[Var] -> a -> a
erase [] a
t = a
t
erase [Var]
xs a
t = forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
sub a
t
  where
    sub :: Subst f
sub = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
undefined forall a b. (a -> b) -> a -> b
$ forall f. [(Var, Term f)] -> Maybe (Subst f)
listToSubst [(Var
x, forall f. Minimal f => Term f
minimalTerm) | Var
x <- [Var]
xs]

-- | Erase all except a given set of variables from the argument, replacing them
-- with the minimal constant.
eraseExcept :: (Symbolic a, ConstantOf a ~ f, Minimal f) => [Var] -> a -> a
eraseExcept :: forall a f.
(Symbolic a, ConstantOf a ~ f, Minimal f) =>
[Var] -> a -> a
eraseExcept [Var]
xs a
t =
  forall a f.
(Symbolic a, ConstantOf a ~ f, Minimal f) =>
[Var] -> a -> a
erase (forall a. Ord a => [a] -> [a]
usort (forall a. Symbolic a => a -> [Var]
vars a
t) forall a. Eq a => [a] -> [a] -> [a]
\\ [Var]
xs) a
t

-- | Replace all variables in the argument with the minimal constant.
ground :: (Symbolic a, ConstantOf a ~ f, Minimal f) => a -> a
ground :: forall a f. (Symbolic a, ConstantOf a ~ f, Minimal f) => a -> a
ground a
t = forall a f.
(Symbolic a, ConstantOf a ~ f, Minimal f) =>
[Var] -> a -> a
erase (forall a. Symbolic a => a -> [Var]
vars a
t) a
t

-- | For types which have a notion of size.
-- | The collection of constraints which the type of function symbols must
-- satisfy in order to be used by twee.
type Function f = (Ordered f, Minimal f, PrettyTerm f, EqualsBonus f, Labelled f)

-- | A hack for encoding Horn clauses. See 'Twee.CP.Score'.
-- The default implementation of 'hasEqualsBonus' should work OK.
class EqualsBonus f where
  hasEqualsBonus :: f -> Bool
  hasEqualsBonus f
_ = Bool
False
  isEquals, isTrue, isFalse :: f -> Bool
  isEquals f
_ = Bool
False
  isTrue f
_ = Bool
False
  isFalse f
_ = Bool
False

instance (Labelled f, EqualsBonus f) => EqualsBonus (Fun f) where
  hasEqualsBonus :: Fun f -> Bool
hasEqualsBonus = forall f. EqualsBonus f => f -> Bool
hasEqualsBonus forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. Labelled f => Fun f -> f
fun_value
  isEquals :: Fun f -> Bool
isEquals = forall f. EqualsBonus f => f -> Bool
isEquals forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. Labelled f => Fun f -> f
fun_value
  isTrue :: Fun f -> Bool
isTrue = forall f. EqualsBonus f => f -> Bool
isTrue forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. Labelled f => Fun f -> f
fun_value
  isFalse :: Fun f -> Bool
isFalse = forall f. EqualsBonus f => f -> Bool
isFalse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. Labelled f => Fun f -> f
fun_value