{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveFunctor      #-}

module AlgebraCheckers.Types where

import Data.Data
import AlgebraCheckers.Unification
import Language.Haskell.TH

data Law a = Law
  { Law a -> a
lawData :: a
  , Law a -> Exp
lawLhsExp :: Exp
  , Law a -> Exp
lawRhsExp :: Exp
  }
  deriving (Eq (Law a)
Eq (Law a)
-> (Law a -> Law a -> Ordering)
-> (Law a -> Law a -> Bool)
-> (Law a -> Law a -> Bool)
-> (Law a -> Law a -> Bool)
-> (Law a -> Law a -> Bool)
-> (Law a -> Law a -> Law a)
-> (Law a -> Law a -> Law a)
-> Ord (Law a)
Law a -> Law a -> Bool
Law a -> Law a -> Ordering
Law a -> Law a -> Law a
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
forall a. Ord a => Eq (Law a)
forall a. Ord a => Law a -> Law a -> Bool
forall a. Ord a => Law a -> Law a -> Ordering
forall a. Ord a => Law a -> Law a -> Law a
min :: Law a -> Law a -> Law a
$cmin :: forall a. Ord a => Law a -> Law a -> Law a
max :: Law a -> Law a -> Law a
$cmax :: forall a. Ord a => Law a -> Law a -> Law a
>= :: Law a -> Law a -> Bool
$c>= :: forall a. Ord a => Law a -> Law a -> Bool
> :: Law a -> Law a -> Bool
$c> :: forall a. Ord a => Law a -> Law a -> Bool
<= :: Law a -> Law a -> Bool
$c<= :: forall a. Ord a => Law a -> Law a -> Bool
< :: Law a -> Law a -> Bool
$c< :: forall a. Ord a => Law a -> Law a -> Bool
compare :: Law a -> Law a -> Ordering
$ccompare :: forall a. Ord a => Law a -> Law a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (Law a)
Ord, Int -> Law a -> ShowS
[Law a] -> ShowS
Law a -> String
(Int -> Law a -> ShowS)
-> (Law a -> String) -> ([Law a] -> ShowS) -> Show (Law a)
forall a. Show a => Int -> Law a -> ShowS
forall a. Show a => [Law a] -> ShowS
forall a. Show a => Law a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Law a] -> ShowS
$cshowList :: forall a. Show a => [Law a] -> ShowS
show :: Law a -> String
$cshow :: forall a. Show a => Law a -> String
showsPrec :: Int -> Law a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Law a -> ShowS
Show, Typeable (Law a)
DataType
Constr
Typeable (Law a)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Law a -> c (Law a))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Law a))
-> (Law a -> Constr)
-> (Law a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Law a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Law a)))
-> ((forall b. Data b => b -> b) -> Law a -> Law a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Law a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Law a -> r)
-> (forall u. (forall d. Data d => d -> u) -> Law a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Law a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Law a -> m (Law a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Law a -> m (Law a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Law a -> m (Law a))
-> Data (Law a)
Law a -> DataType
Law a -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (Law a))
(forall b. Data b => b -> b) -> Law a -> Law a
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Law a -> c (Law a)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Law a)
forall a. Data a => Typeable (Law a)
forall a. Data a => Law a -> DataType
forall a. Data a => Law a -> Constr
forall a. Data a => (forall b. Data b => b -> b) -> Law a -> Law a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Law a -> u
forall a u. Data a => (forall d. Data d => d -> u) -> Law a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Law a -> r
forall a r r'.
Data a =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Law a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Law a -> m (Law a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Law a -> m (Law a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Law a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Law a -> c (Law a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Law a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Law a))
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Law a -> u
forall u. (forall d. Data d => d -> u) -> Law a -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Law a -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Law a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Law a -> m (Law a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Law a -> m (Law a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Law a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Law a -> c (Law a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Law a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Law a))
$cLaw :: Constr
$tLaw :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Law a -> m (Law a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Law a -> m (Law a)
gmapMp :: (forall d. Data d => d -> m d) -> Law a -> m (Law a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Law a -> m (Law a)
gmapM :: (forall d. Data d => d -> m d) -> Law a -> m (Law a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Law a -> m (Law a)
gmapQi :: Int -> (forall d. Data d => d -> u) -> Law a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Law a -> u
gmapQ :: (forall d. Data d => d -> u) -> Law a -> [u]
$cgmapQ :: forall a u. Data a => (forall d. Data d => d -> u) -> Law a -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Law a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Law a -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Law a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Law a -> r
gmapT :: (forall b. Data b => b -> b) -> Law a -> Law a
$cgmapT :: forall a. Data a => (forall b. Data b => b -> b) -> Law a -> Law a
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Law a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Law a))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (Law a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Law a))
dataTypeOf :: Law a -> DataType
$cdataTypeOf :: forall a. Data a => Law a -> DataType
toConstr :: Law a -> Constr
$ctoConstr :: forall a. Data a => Law a -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Law a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Law a)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Law a -> c (Law a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Law a -> c (Law a)
$cp1Data :: forall a. Data a => Typeable (Law a)
Data, Typeable)

instance Eq a => Eq (Law a) where
  Law a
_ Exp
a Exp
a' == :: Law a -> Law a -> Bool
== Law a
_ Exp
b Exp
b' =
    [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
      [ Exp -> Exp -> Bool
equalUpToAlpha Exp
a Exp
b Bool -> Bool -> Bool
&& Exp -> Exp -> Bool
equalUpToAlpha Exp
a' Exp
b'
      ]

data LawSort
  = LawName String
  | LawNotDodgy
  deriving (LawSort -> LawSort -> Bool
(LawSort -> LawSort -> Bool)
-> (LawSort -> LawSort -> Bool) -> Eq LawSort
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LawSort -> LawSort -> Bool
$c/= :: LawSort -> LawSort -> Bool
== :: LawSort -> LawSort -> Bool
$c== :: LawSort -> LawSort -> Bool
Eq, Eq LawSort
Eq LawSort
-> (LawSort -> LawSort -> Ordering)
-> (LawSort -> LawSort -> Bool)
-> (LawSort -> LawSort -> Bool)
-> (LawSort -> LawSort -> Bool)
-> (LawSort -> LawSort -> Bool)
-> (LawSort -> LawSort -> LawSort)
-> (LawSort -> LawSort -> LawSort)
-> Ord LawSort
LawSort -> LawSort -> Bool
LawSort -> LawSort -> Ordering
LawSort -> LawSort -> LawSort
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 :: LawSort -> LawSort -> LawSort
$cmin :: LawSort -> LawSort -> LawSort
max :: LawSort -> LawSort -> LawSort
$cmax :: LawSort -> LawSort -> LawSort
>= :: LawSort -> LawSort -> Bool
$c>= :: LawSort -> LawSort -> Bool
> :: LawSort -> LawSort -> Bool
$c> :: LawSort -> LawSort -> Bool
<= :: LawSort -> LawSort -> Bool
$c<= :: LawSort -> LawSort -> Bool
< :: LawSort -> LawSort -> Bool
$c< :: LawSort -> LawSort -> Bool
compare :: LawSort -> LawSort -> Ordering
$ccompare :: LawSort -> LawSort -> Ordering
$cp1Ord :: Eq LawSort
Ord, Int -> LawSort -> ShowS
[LawSort] -> ShowS
LawSort -> String
(Int -> LawSort -> ShowS)
-> (LawSort -> String) -> ([LawSort] -> ShowS) -> Show LawSort
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LawSort] -> ShowS
$cshowList :: [LawSort] -> ShowS
show :: LawSort -> String
$cshow :: LawSort -> String
showsPrec :: Int -> LawSort -> ShowS
$cshowsPrec :: Int -> LawSort -> ShowS
Show)

type NamedLaw = Law LawSort
type Theorem  = Law TheoremSource

data Arity = Binary | Prefix Int
  deriving (Arity -> Arity -> Bool
(Arity -> Arity -> Bool) -> (Arity -> Arity -> Bool) -> Eq Arity
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Arity -> Arity -> Bool
$c/= :: Arity -> Arity -> Bool
== :: Arity -> Arity -> Bool
$c== :: Arity -> Arity -> Bool
Eq, Eq Arity
Eq Arity
-> (Arity -> Arity -> Ordering)
-> (Arity -> Arity -> Bool)
-> (Arity -> Arity -> Bool)
-> (Arity -> Arity -> Bool)
-> (Arity -> Arity -> Bool)
-> (Arity -> Arity -> Arity)
-> (Arity -> Arity -> Arity)
-> Ord Arity
Arity -> Arity -> Bool
Arity -> Arity -> Ordering
Arity -> Arity -> Arity
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 :: Arity -> Arity -> Arity
$cmin :: Arity -> Arity -> Arity
max :: Arity -> Arity -> Arity
$cmax :: Arity -> Arity -> Arity
>= :: Arity -> Arity -> Bool
$c>= :: Arity -> Arity -> Bool
> :: Arity -> Arity -> Bool
$c> :: Arity -> Arity -> Bool
<= :: Arity -> Arity -> Bool
$c<= :: Arity -> Arity -> Bool
< :: Arity -> Arity -> Bool
$c< :: Arity -> Arity -> Bool
compare :: Arity -> Arity -> Ordering
$ccompare :: Arity -> Arity -> Ordering
$cp1Ord :: Eq Arity
Ord, Int -> Arity -> ShowS
[Arity] -> ShowS
Arity -> String
(Int -> Arity -> ShowS)
-> (Arity -> String) -> ([Arity] -> ShowS) -> Show Arity
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Arity] -> ShowS
$cshowList :: [Arity] -> ShowS
show :: Arity -> String
$cshow :: Arity -> String
showsPrec :: Int -> Arity -> ShowS
$cshowsPrec :: Int -> Arity -> ShowS
Show)

data TheoremProblem
  = Dodgy DodgyReason
  | Contradiction ContradictionReason
  deriving (TheoremProblem -> TheoremProblem -> Bool
(TheoremProblem -> TheoremProblem -> Bool)
-> (TheoremProblem -> TheoremProblem -> Bool) -> Eq TheoremProblem
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TheoremProblem -> TheoremProblem -> Bool
$c/= :: TheoremProblem -> TheoremProblem -> Bool
== :: TheoremProblem -> TheoremProblem -> Bool
$c== :: TheoremProblem -> TheoremProblem -> Bool
Eq, Eq TheoremProblem
Eq TheoremProblem
-> (TheoremProblem -> TheoremProblem -> Ordering)
-> (TheoremProblem -> TheoremProblem -> Bool)
-> (TheoremProblem -> TheoremProblem -> Bool)
-> (TheoremProblem -> TheoremProblem -> Bool)
-> (TheoremProblem -> TheoremProblem -> Bool)
-> (TheoremProblem -> TheoremProblem -> TheoremProblem)
-> (TheoremProblem -> TheoremProblem -> TheoremProblem)
-> Ord TheoremProblem
TheoremProblem -> TheoremProblem -> Bool
TheoremProblem -> TheoremProblem -> Ordering
TheoremProblem -> TheoremProblem -> TheoremProblem
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 :: TheoremProblem -> TheoremProblem -> TheoremProblem
$cmin :: TheoremProblem -> TheoremProblem -> TheoremProblem
max :: TheoremProblem -> TheoremProblem -> TheoremProblem
$cmax :: TheoremProblem -> TheoremProblem -> TheoremProblem
>= :: TheoremProblem -> TheoremProblem -> Bool
$c>= :: TheoremProblem -> TheoremProblem -> Bool
> :: TheoremProblem -> TheoremProblem -> Bool
$c> :: TheoremProblem -> TheoremProblem -> Bool
<= :: TheoremProblem -> TheoremProblem -> Bool
$c<= :: TheoremProblem -> TheoremProblem -> Bool
< :: TheoremProblem -> TheoremProblem -> Bool
$c< :: TheoremProblem -> TheoremProblem -> Bool
compare :: TheoremProblem -> TheoremProblem -> Ordering
$ccompare :: TheoremProblem -> TheoremProblem -> Ordering
$cp1Ord :: Eq TheoremProblem
Ord, Int -> TheoremProblem -> ShowS
[TheoremProblem] -> ShowS
TheoremProblem -> String
(Int -> TheoremProblem -> ShowS)
-> (TheoremProblem -> String)
-> ([TheoremProblem] -> ShowS)
-> Show TheoremProblem
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TheoremProblem] -> ShowS
$cshowList :: [TheoremProblem] -> ShowS
show :: TheoremProblem -> String
$cshow :: TheoremProblem -> String
showsPrec :: Int -> TheoremProblem -> ShowS
$cshowsPrec :: Int -> TheoremProblem -> ShowS
Show)

isContradiction :: TheoremProblem -> Bool
isContradiction :: TheoremProblem -> Bool
isContradiction Contradiction{} = Bool
True
isContradiction TheoremProblem
_               = Bool
False

isDodgy :: TheoremProblem -> Bool
isDodgy :: TheoremProblem -> Bool
isDodgy Dodgy{} = Bool
True
isDodgy TheoremProblem
_       = Bool
False

data ContradictionReason
  = UnboundMatchableVars [Name]
  | UnequalValues
  | UnknownConstructors [Name]
  deriving (ContradictionReason -> ContradictionReason -> Bool
(ContradictionReason -> ContradictionReason -> Bool)
-> (ContradictionReason -> ContradictionReason -> Bool)
-> Eq ContradictionReason
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ContradictionReason -> ContradictionReason -> Bool
$c/= :: ContradictionReason -> ContradictionReason -> Bool
== :: ContradictionReason -> ContradictionReason -> Bool
$c== :: ContradictionReason -> ContradictionReason -> Bool
Eq, Eq ContradictionReason
Eq ContradictionReason
-> (ContradictionReason -> ContradictionReason -> Ordering)
-> (ContradictionReason -> ContradictionReason -> Bool)
-> (ContradictionReason -> ContradictionReason -> Bool)
-> (ContradictionReason -> ContradictionReason -> Bool)
-> (ContradictionReason -> ContradictionReason -> Bool)
-> (ContradictionReason
    -> ContradictionReason -> ContradictionReason)
-> (ContradictionReason
    -> ContradictionReason -> ContradictionReason)
-> Ord ContradictionReason
ContradictionReason -> ContradictionReason -> Bool
ContradictionReason -> ContradictionReason -> Ordering
ContradictionReason -> ContradictionReason -> ContradictionReason
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 :: ContradictionReason -> ContradictionReason -> ContradictionReason
$cmin :: ContradictionReason -> ContradictionReason -> ContradictionReason
max :: ContradictionReason -> ContradictionReason -> ContradictionReason
$cmax :: ContradictionReason -> ContradictionReason -> ContradictionReason
>= :: ContradictionReason -> ContradictionReason -> Bool
$c>= :: ContradictionReason -> ContradictionReason -> Bool
> :: ContradictionReason -> ContradictionReason -> Bool
$c> :: ContradictionReason -> ContradictionReason -> Bool
<= :: ContradictionReason -> ContradictionReason -> Bool
$c<= :: ContradictionReason -> ContradictionReason -> Bool
< :: ContradictionReason -> ContradictionReason -> Bool
$c< :: ContradictionReason -> ContradictionReason -> Bool
compare :: ContradictionReason -> ContradictionReason -> Ordering
$ccompare :: ContradictionReason -> ContradictionReason -> Ordering
$cp1Ord :: Eq ContradictionReason
Ord, Int -> ContradictionReason -> ShowS
[ContradictionReason] -> ShowS
ContradictionReason -> String
(Int -> ContradictionReason -> ShowS)
-> (ContradictionReason -> String)
-> ([ContradictionReason] -> ShowS)
-> Show ContradictionReason
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ContradictionReason] -> ShowS
$cshowList :: [ContradictionReason] -> ShowS
show :: ContradictionReason -> String
$cshow :: ContradictionReason -> String
showsPrec :: Int -> ContradictionReason -> ShowS
$cshowsPrec :: Int -> ContradictionReason -> ShowS
Show)

data DodgyReason
  = SelfRecursive
  deriving (DodgyReason -> DodgyReason -> Bool
(DodgyReason -> DodgyReason -> Bool)
-> (DodgyReason -> DodgyReason -> Bool) -> Eq DodgyReason
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DodgyReason -> DodgyReason -> Bool
$c/= :: DodgyReason -> DodgyReason -> Bool
== :: DodgyReason -> DodgyReason -> Bool
$c== :: DodgyReason -> DodgyReason -> Bool
Eq, Eq DodgyReason
Eq DodgyReason
-> (DodgyReason -> DodgyReason -> Ordering)
-> (DodgyReason -> DodgyReason -> Bool)
-> (DodgyReason -> DodgyReason -> Bool)
-> (DodgyReason -> DodgyReason -> Bool)
-> (DodgyReason -> DodgyReason -> Bool)
-> (DodgyReason -> DodgyReason -> DodgyReason)
-> (DodgyReason -> DodgyReason -> DodgyReason)
-> Ord DodgyReason
DodgyReason -> DodgyReason -> Bool
DodgyReason -> DodgyReason -> Ordering
DodgyReason -> DodgyReason -> DodgyReason
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 :: DodgyReason -> DodgyReason -> DodgyReason
$cmin :: DodgyReason -> DodgyReason -> DodgyReason
max :: DodgyReason -> DodgyReason -> DodgyReason
$cmax :: DodgyReason -> DodgyReason -> DodgyReason
>= :: DodgyReason -> DodgyReason -> Bool
$c>= :: DodgyReason -> DodgyReason -> Bool
> :: DodgyReason -> DodgyReason -> Bool
$c> :: DodgyReason -> DodgyReason -> Bool
<= :: DodgyReason -> DodgyReason -> Bool
$c<= :: DodgyReason -> DodgyReason -> Bool
< :: DodgyReason -> DodgyReason -> Bool
$c< :: DodgyReason -> DodgyReason -> Bool
compare :: DodgyReason -> DodgyReason -> Ordering
$ccompare :: DodgyReason -> DodgyReason -> Ordering
$cp1Ord :: Eq DodgyReason
Ord, Int -> DodgyReason -> ShowS
[DodgyReason] -> ShowS
DodgyReason -> String
(Int -> DodgyReason -> ShowS)
-> (DodgyReason -> String)
-> ([DodgyReason] -> ShowS)
-> Show DodgyReason
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DodgyReason] -> ShowS
$cshowList :: [DodgyReason] -> ShowS
show :: DodgyReason -> String
$cshow :: DodgyReason -> String
showsPrec :: Int -> DodgyReason -> ShowS
$cshowsPrec :: Int -> DodgyReason -> ShowS
Show)

data TheoremSource
  = LawDefn String
  | Interaction String String
  deriving (TheoremSource -> TheoremSource -> Bool
(TheoremSource -> TheoremSource -> Bool)
-> (TheoremSource -> TheoremSource -> Bool) -> Eq TheoremSource
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TheoremSource -> TheoremSource -> Bool
$c/= :: TheoremSource -> TheoremSource -> Bool
== :: TheoremSource -> TheoremSource -> Bool
$c== :: TheoremSource -> TheoremSource -> Bool
Eq, Eq TheoremSource
Eq TheoremSource
-> (TheoremSource -> TheoremSource -> Ordering)
-> (TheoremSource -> TheoremSource -> Bool)
-> (TheoremSource -> TheoremSource -> Bool)
-> (TheoremSource -> TheoremSource -> Bool)
-> (TheoremSource -> TheoremSource -> Bool)
-> (TheoremSource -> TheoremSource -> TheoremSource)
-> (TheoremSource -> TheoremSource -> TheoremSource)
-> Ord TheoremSource
TheoremSource -> TheoremSource -> Bool
TheoremSource -> TheoremSource -> Ordering
TheoremSource -> TheoremSource -> TheoremSource
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 :: TheoremSource -> TheoremSource -> TheoremSource
$cmin :: TheoremSource -> TheoremSource -> TheoremSource
max :: TheoremSource -> TheoremSource -> TheoremSource
$cmax :: TheoremSource -> TheoremSource -> TheoremSource
>= :: TheoremSource -> TheoremSource -> Bool
$c>= :: TheoremSource -> TheoremSource -> Bool
> :: TheoremSource -> TheoremSource -> Bool
$c> :: TheoremSource -> TheoremSource -> Bool
<= :: TheoremSource -> TheoremSource -> Bool
$c<= :: TheoremSource -> TheoremSource -> Bool
< :: TheoremSource -> TheoremSource -> Bool
$c< :: TheoremSource -> TheoremSource -> Bool
compare :: TheoremSource -> TheoremSource -> Ordering
$ccompare :: TheoremSource -> TheoremSource -> Ordering
$cp1Ord :: Eq TheoremSource
Ord, Int -> TheoremSource -> ShowS
[TheoremSource] -> ShowS
TheoremSource -> String
(Int -> TheoremSource -> ShowS)
-> (TheoremSource -> String)
-> ([TheoremSource] -> ShowS)
-> Show TheoremSource
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TheoremSource] -> ShowS
$cshowList :: [TheoremSource] -> ShowS
show :: TheoremSource -> String
$cshow :: TheoremSource -> String
showsPrec :: Int -> TheoremSource -> ShowS
$cshowsPrec :: Int -> TheoremSource -> ShowS
Show)