Types.hs

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

module AlgebraCheckers.Types where

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

data Law a = Law
  { lawData :: a
  , lawLhsExp :: Exp
  , lawRhsExp :: Exp
  }
  deriving (Ord, Show, Data, Typeable)

instance Eq a => Eq (Law a) where
  Law _ a a' == Law _ b b' =
    and
      [ equalUpToAlpha a b && equalUpToAlpha a' b'
      ]

data LawSort
  = LawName String
  | LawNotDodgy
  deriving (Eq, Ord, Show)

type NamedLaw = Law LawSort
type Theorem  = Law TheoremSource

data Arity = Binary | Prefix Int
  deriving (Eq, Ord, Show)

data TheoremProblem
  = Dodgy DodgyReason
  | Contradiction ContradictionReason
  deriving (Eq, Ord, Show)

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

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

data ContradictionReason
  = UnboundMatchableVars [Name]
  | UnequalValues
  | UnknownConstructors [Name]
  deriving (Eq, Ord, Show)

data DodgyReason
  = SelfRecursive
  deriving (Eq, Ord, Show)

data TheoremSource
  = LawDefn String
  | Interaction String String
  deriving (Eq, Ord, Show)